changed names of resource-1.3; added a note on homepage on release

12 files changed, 0 insertions, 516 deletions

diff --git a/examples/logic/Arithm.gf b/examples/logic/Arithm.gf
deleted file mode 100644
index 331a0d7c6..000000000
--- a/examples/logic/Arithm.gf
+++ /dev/null
@@ -1,64 +0,0 @@
-abstract Arithm = Logic ** {
-
--- arithmetic
-fun 
-  Nat  : Dom ;
-data
-  Zero : Elem Nat ;
-  Succ : Elem Nat -> Elem Nat ;
-fun
-  EqNat : (m,n : Elem Nat) -> Prop ;
-  LtNat : (m,n : Elem Nat) -> Prop ;
-  Div   : (m,n : Elem Nat) -> Prop ;
-  Even  : Elem Nat -> Prop ;
-  Odd   : Elem Nat -> Prop ;
-  Prime : Elem Nat -> Prop ;
-
-  one  : Elem Nat ;
-  two  : Elem Nat ;
-  sum  : (m,n : Elem Nat) -> Elem Nat ;
-  prod : (m,n : Elem Nat) -> Elem Nat ;
-data
-  evax1 : Proof (Even Zero) ;
-  evax2 : (n : Elem Nat) -> Proof (Even n) -> Proof (Odd (Succ n)) ;
-  evax3 : (n : Elem Nat) -> Proof (Odd n)  -> Proof (Even (Succ n)) ;
-
-  eqax1 : Proof (EqNat Zero Zero) ;
-  eqax2 : (m,n : Elem Nat) -> Proof (EqNat m n) -> 
-             Proof (EqNat (Succ m) (Succ n)) ;
-fun
-  IndNat : (C : Elem Nat -> Prop) -> 
-             Proof (C Zero) -> 
-             ((x : Elem Nat) -> Hypo (C x) -> Proof (C (Succ x))) -> 
-                Proof (Univ Nat C) ;
-
-def 
-  one = Succ Zero ;
-  two = Succ one ;
-  sum m (Succ n) = Succ (sum m n) ;
-  sum m Zero = m ;
-  prod m (Succ n) = sum (prod m n) m ;
-  prod m Zero = Zero ;
-  LtNat m n = Exist Nat (\x -> EqNat n (sum m (Succ x))) ;
-  Div m n = Exist Nat (\x -> EqNat m (prod x n)) ;
-  Prime n = 
-    Conj (LtNat one n) 
-           (Univ Nat (\x -> Impl (Conj (LtNat one x) (Div n x)) (EqNat x n))) ;
-
-fun ex1 : Text ;
-def ex1 = 
-  ThmWithProof 
-    (Univ Nat (\x -> Disj (Even x) (Odd x))) 
-    (IndNat 
-       (\x -> Disj (Even x) (Odd x)) 
-       (DisjIl (Even Zero) (Odd Zero) evax1) 
-       (\x -> \h -> DisjE (Even x) (Odd x) (Disj (Even (Succ x)) (Odd (Succ x)))
-         (Hypoth (Disj (Even x) (Odd x)) h) 
-         (\a -> DisjIr (Even (Succ x)) (Odd (Succ x)) 
-            (evax2 x (Hypoth (Even x) a))) 
-         (\b -> DisjIl (Even (Succ x)) (Odd (Succ x)) 
-            (evax3 x (Hypoth (Odd x) b))
-         )
-       )
-     ) ;
-} ;
diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf
deleted file mode 100644
index 942b6d7c2..000000000
--- a/examples/logic/ArithmEng.gf
+++ /dev/null
@@ -1,66 +0,0 @@
---# -path=.:mathematical:present:prelude
-
-concrete ArithmEng of Arithm = LogicEng ** 
-  open
-    GrammarEng,
-    ParadigmsEng,
-    ProoftextEng,
-    MathematicalEng,
-    CombinatorsEng,
-    ConstructorsEng
-  in { 
-
-lin
-  Nat  = UseN  (regN "number") ;
-  Zero = UsePN (regPN "zero") ;
-  Succ = appN2 (regN2 "successor") ;
-
-  EqNat x y = mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) x y) ;
-  LtNat x y = mkS (predAComp (regA "equal") x y) ;
-  Div   x y = mkS (predA2 (mkA2 (regA "divisible") (mkPrep "by")) x y) ;
-  Even  x = mkS (predA (regA "even") x) ;
-  Odd   x = mkS (predA (regA "odd") x) ;
-  Prime x = mkS (predA (regA "prime") x) ;
-
-  one = UsePN (regPN "one") ;
-  two = UsePN (regPN "two") ;
-  sum = app (regN2 "sum") ;
-  prod = app (regN2 "product") ;
-
-  evax1 = 
-    proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) 
-      (mkS (predA (regA "even") (UsePN (regPN "zero")))) ;
-  evax2 n c = 
-    appendText c 
-      (proof (by (ref (mkLabel ["the second axiom of evenness ,"]))) 
-        (mkS (predA (regA "odd") (appN2 (regN2 "successor") n)))) ;
-  evax3 n c = 
-    appendText c 
-      (proof (by (ref (mkLabel ["the third axiom of evenness ,"]))) 
-        (mkS (predA (regA "even") (appN2 (regN2 "successor") n)))) ;
-
-
-  eqax1 = 
-    proof (by (ref (mkLabel ["the first axiom of equality ,"]))) 
-      (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) 
-         (UsePN (regPN "zero")) 
-         (UsePN (regPN "zero")))) ;
-
-  eqax2 m n c = 
-    appendText c 
-      (proof (by (ref (mkLabel ["the second axiom of equality ,"]))) 
-        (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) 
-          (appN2 (regN2 "successor") m) (appN2 (regN2 "successor") n)))) ;
-
-  IndNat C d e = {s = 
-    ["we proceed by induction . for the basis ,"] ++ d.s ++ 
-    ["for the induction step, consider a number"] ++ C.$0 ++ 
-    ["and assume"] ++ C.s ++ 
-    --- "(" ++ e.$1 ++ ")" ++ 
-    "." ++ e.s ++ 
-    ["hence , for all numbers"] ++ C.$0 ++ "," ++ C.s ; lock_Text = <>} ;
-
-  ex1 = proof ["the first theorem and its proof"] ;
-
-} ;
-
diff --git a/examples/logic/LexTheory.gf b/examples/logic/LexTheory.gf
deleted file mode 100644
index a7a7c9439..000000000
--- a/examples/logic/LexTheory.gf
+++ /dev/null
@@ -1,13 +0,0 @@
-interface LexTheory = open Grammar in {
-
-  oper
-    assume_VS : VS ;
-    case_N : N ;
-    contradiction_N : N ;
-    have_V2 : V2 ;
-    hypothesis_N : N ;
-    ifthen_DConj : DConj ;
-
-    defNP : Str -> NP ;
-
-}
diff --git a/examples/logic/LexTheoryEng.gf b/examples/logic/LexTheoryEng.gf
deleted file mode 100644
index 165e1796d..000000000
--- a/examples/logic/LexTheoryEng.gf
+++ /dev/null
@@ -1,13 +0,0 @@
-instance LexTheoryEng of LexTheory = open 
-  GrammarEng, ParadigmsEng, IrregEng, ParamX in {
-  oper
-    assume_VS = mkVS (regV "assume") ;
-    case_N = regN "case" ;
-    contradiction_N = regN "contradiction" ;
-    have_V2 = dirV2 have_V ;
-    hypothesis_N = mk2N "hypothesis" "hypotheses" ;
-    ifthen_DConj = {s1 = "if" ; s2 = "then" ; n = singular ; lock_DConj = <>} ;
-
-    defNP s = {s = \\_ => s ; a = {n = Sg ; p = P3} ; lock_NP = <>} ;
-
-}
diff --git a/examples/logic/Logic.gf b/examples/logic/Logic.gf
deleted file mode 100644
index f7bb4ab57..000000000
--- a/examples/logic/Logic.gf
+++ /dev/null
@@ -1,60 +0,0 @@
--- many-sorted predicate calculus
--- AR 1999, revised 2001 and 2006
-
-abstract Logic = {
-
-cat 
-  Prop ;       -- proposition
-  Dom ;        -- domain of quantification
-  Elem Dom ;   -- individual element of a domain
-  Proof Prop ; -- proof of a proposition
-  Hypo Prop ;  -- hypothesis of a proposition
-  Text ;       -- theorem with proof etc. 
-
-fun 
-  -- texts
-  Statement : Prop -> Text ;
-  ThmWithProof : (A : Prop) -> Proof A -> Text ;
-  ThmWithTrivialProof : (A : Prop) -> Proof A -> Text ;
-
-  -- logically complex propositions
-  Disj : (A,B : Prop) -> Prop ;
-  Conj : (A,B : Prop) -> Prop ;
-  Impl : (A,B : Prop) -> Prop ;
-  Abs  : Prop ;
-  Neg  : Prop -> Prop ;
-
-  Univ  : (A : Dom) -> (Elem A -> Prop) -> Prop ;
-  Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ;
- 
-  -- inference rules
-
-  ConjI  : (A,B : Prop) -> Proof A -> Proof B -> Proof (Conj A B) ;  
-  ConjEl : (A,B : Prop) -> Proof (Conj A B) -> Proof A ;
-  ConjEr : (A,B : Prop) -> Proof (Conj A B) -> Proof B ;
-  DisjIl : (A,B : Prop) -> Proof A -> Proof (Disj A B) ;
-  DisjIr : (A,B : Prop) -> Proof B -> Proof (Disj A B) ;
-  DisjE  : (A,B,C : Prop) -> Proof (Disj A B) -> 
-              (Hypo A -> Proof C) -> (Hypo B -> Proof C) -> Proof C ;
-  ImplI  : (A,B : Prop) -> (Hypo A -> Proof B) -> Proof (Impl A B) ;
-  ImplE  : (A,B : Prop) -> Proof (Impl A B) -> Proof A -> Proof B ;
-  NegI   : (A : Prop) -> (Hypo A -> Proof Abs) -> Proof (Neg A) ;
-  NegE   : (A : Prop) -> Proof (Neg A) -> Proof A -> Proof Abs ;
-  AbsE   : (C : Prop) -> Proof Abs -> Proof C ;
-  UnivI  : (A : Dom) -> (B : Elem A -> Prop) -> 
-              ((x : Elem A) -> Proof (B x)) -> Proof (Univ A B) ;
-  UnivE  : (A : Dom) -> (B : Elem A -> Prop) -> 
-              Proof (Univ A B) -> (a : Elem A) -> Proof (B a) ;
-  ExistI : (A : Dom) -> (B : Elem A -> Prop) -> 
-              (a : Elem A) -> Proof (B a) -> Proof (Exist A B) ;
-  ExistE : (A : Dom) -> (B : Elem A -> Prop) -> (C : Prop) -> 
-              Proof (Exist A B) -> ((x : Elem A) -> Proof (B x) -> Proof C) -> 
-              Proof C ;
-
-  -- use a hypothesis
-  Hypoth : (A : Prop) -> Hypo A -> Proof A ;
-
-  -- pronoun
-  Pron : (A : Dom) -> Elem A -> Elem A ;
-
-} ;
diff --git a/examples/logic/LogicEng.gf b/examples/logic/LogicEng.gf
deleted file mode 100644
index 18f466fa7..000000000
--- a/examples/logic/LogicEng.gf
+++ /dev/null
@@ -1,23 +0,0 @@
---# -path=.:mathematical:present:resource-1.0/api:prelude
-
-concrete LogicEng of Logic = LogicI with
-  (LexTheory = LexTheoryEng), 
-  (Prooftext = ProoftextEng),
-  (Grammar = GrammarEng), 
-  (Symbolic = SymbolicEng), 
-  (Symbol = SymbolEng), 
-  (Combinators = CombinatorsEng), 
-  (Constructors = ConstructorsEng), 
-  ;
-
-{-
-ImplI Abs Abs (\h -> DisjE Abs Abs Abs (DisjIr Abs Abs (Hypoth Abs h)) 
-(\x -> Hypoth Abs x) (\y -> Hypoth Abs y))
-
-assume that we have a contradiction . by the hypothesis we have a contradiction . 
-a fortiori we have a contradiction or we have a contradiction . 
-we have two cases. assume that we have a contradiction . 
-by the hypothesis we have a contradiction . assume that we have a contradiction . 
-by the hypothesis we have a contradiction . therefore we have a contradiction . 
-therefore if we have a contradiction then we have a contradiction .
--}
diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf
deleted file mode 100644
index 3598022ac..000000000
--- a/examples/logic/LogicI.gf
+++ /dev/null
@@ -1,59 +0,0 @@
-incomplete concrete LogicI of Logic = 
-  open 
-    LexTheory,
-    Prooftext, 
-    Grammar, 
-    Constructors, 
-    Combinators
-  in {
-
-lincat 
-  Prop  = Prooftext.Prop ;
-  Proof = Prooftext.Proof ;
-  Dom   = Typ ;
-  Elem  = Object ;
-  Hypo  = Label ;
-  Text  = Section ;
-
-lin
-  ThmWithProof = theorem ;
-
-  Conj = coord and_Conj ;
-  Disj = coord or_Conj ;
-  Impl = coord ifthen_DConj ;
-
-  Abs = 
-    mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
-
-  Univ A B = 
-    AdvS 
-      (mkAdv for_Prep (mkNP all_Predet 
-        (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0)))))
-      B ;
-
-  DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
-  DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ;
-
-  DisjE A B C c d e =
-    appendText
-      c 
-      (appendText
-        (appendText
-           (cases (mkNum n2)) 
-           (proofs 
-             (appendText (assumption A) d)
-             (appendText (assumption B) e)))
-        (proof therefore C)) ;
-
-  ImplI A B b = 
-    proof 
-      (assumption A) 
-      (appendText b (proof therefore (coord ifthen_DConj A B))) ;
-
-  Hypoth A h = proof hypothesis A ;
-
-
-lindef
-  Elem = defNP ;
-
-}
diff --git a/examples/logic/Prooftext.gf b/examples/logic/Prooftext.gf
deleted file mode 100644
index 1833d6308..000000000
--- a/examples/logic/Prooftext.gf
+++ /dev/null
@@ -1,86 +0,0 @@
-interface Prooftext = open 
-  Grammar, 
-  LexTheory,
-  Symbolic,
-  Symbol, 
-  (C=ConstructX),
-  Constructors, 
-  Combinators 
-  in {
-
-oper
-  Chapter  = Text ;
-  Section  = Text ;
-  Sections = Text ;
-  Decl     = Text ;
-  Decls    = Text ;
-  Prop     = S ;
-  Branching= S ;
-  Proof    = Text ;
-  Proofs   = Text ;
-  Typ      = CN ;
-  Object   = NP ;
-  Label    = NP ;
-  Adverb   = PConj ;
-  Ref      = NP ;
-  Refs     = [NP] ;
-  Number   = Num ;
-
-  chapter : Label -> Sections -> Chapter 
-    = \title,jments -> 
-        appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ;
-
-  definition : Decls -> Object -> Object -> Section 
-    = \decl,a,b -> 
-        appendText decl (mkText (mkPhr (mkUtt (mkS (pred b a)))) TEmpty) ;
-
-  theorem : Prop -> Proof -> Section 
-    = \prop,prf -> appendText (mkText (mkPhr prop) TEmpty) prf ;
-
-  assumption : Prop -> Decl 
-    = \p -> 
-        mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
-
-  declaration : Object -> Typ -> Decl
-    = \a,ty ->
-        mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ;
-
-  proof = overload {
-    proof : Prop -> Proof 
-      = \p -> mkText (mkPhr p) TEmpty ;
-    proof : Str -> Proof
-      = \s -> {s = s ++ "." ; lock_Text = <>} ;
-    proof : Adverb -> Prop -> Proof
-      = \a,p -> mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
-    proof : Decl -> Proof
-      = \d -> d ;
-    proof : Proof -> Proof -> Proof
-      = appendText ;
-    proof : Branching -> Proofs -> Proof
-      = \b,ps -> mkText (mkPhr b) ps
-    } ;
-
-  proofs : Proof -> Proof -> Proofs 
-    = appendText ;
-
-  cases : Num -> Branching 
-    = \n -> 
-        mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet n) case_N)) ;
-
-  by : Ref -> Adverb 
-    = \h -> C.mkPConj (mkAdv by8means_Prep h).s ;
-  therefore : Adverb
-    = therefore_PConj ;
-  afortiori : Adverb
-    = C.mkPConj ["a fortiori"] ;
-  hypothesis : Adverb
-    = C.mkPConj (mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N)).s ;
-
-  ref : Label -> Ref
-    = \h -> h ;
-  refs : Refs -> Ref
-    = \rs -> mkNP and_Conj rs ;
-
-  mkLabel : Str -> Label ;
-
-}
diff --git a/examples/logic/ProoftextEng.gf b/examples/logic/ProoftextEng.gf
deleted file mode 100644
index 9ccd7a410..000000000
--- a/examples/logic/ProoftextEng.gf
+++ /dev/null
@@ -1,19 +0,0 @@
---# -path=.:mathematical:present:resource-1.0/api:prelude
-
-instance ProoftextEng of Prooftext = 
-  open 
-    LexTheoryEng, 
-    GrammarEng, 
-    SymbolicEng, 
-    SymbolEng, 
-    (C=ConstructX),
-    CombinatorsEng, 
-    ConstructorsEng,
-    (P=ParadigmsEng)
-  in {
-
-oper
-  mkLabel : Str -> Label = \s -> UsePN (P.regPN s) ;
-
-
-}
diff --git a/examples/logic/Theory.gf b/examples/logic/Theory.gf
deleted file mode 100644
index 778e0a8ec..000000000
--- a/examples/logic/Theory.gf
+++ /dev/null
@@ -1,47 +0,0 @@
-abstract Theory = {
-
-  cat
-    Chapter ;
-    Jment ;
-    [Jment] {0} ;
-    Decl ;
-    [Decl] {0} ;
-    Prop ;
-    Proof ;
-    [Proof] {2} ;
-    Branch ;
-    Typ ;
-    Obj ;
-    Label ;
-    Ref ;
-    [Ref] ;
-    Adverb ;
-    Number ;
-    
-  fun
-    Chap       : Label -> [Jment] -> Chapter ;          -- title, text
-
-    JDefObj    : [Decl] -> Obj -> Obj -> Jment ;        -- a = b (G)
-    JDefObjTyp : [Decl] -> Typ -> Obj -> Obj -> Jment ; -- a = b : A (G)
-    JDefProp   : [Decl] -> Prop -> Prop -> Jment ;      -- A = B : Prop (G)
-    JThm       : [Decl] -> Prop -> Proof -> Jment ;     -- p : P (G)
-
-    DProp      : Prop  -> Decl ;                        -- assume P
-    DPropLabel : Label -> Prop -> Label ;               -- assume P (h)
-    DTyp       : Obj   -> Typ -> Decl ;                 -- let x,y be T
-
-    PProp      : Prop -> Proof ;                        -- P.
-    PAdvProp   : Adverb -> Prop -> Proof ;              -- Hence, P.
-    PDecl      : Decl -> Proof ;                        -- Assume P.
-    PBranch    : Branch -> [Proof] -> Proof ;           -- By cases: P1 P2
-
-    BCases     : Number -> Branch ;                     -- We have n cases.
-    
-    ARef       : Ref -> Adverb ;                        -- by Thm 2
-    AHence     : Adverb ;                               -- therefore
-    AAFort     : Adverb ;                               -- a fortiori
-
-    RLabel     : Label -> Ref ;                         -- Thm 2
-    RMany      : [Ref] -> Ref ;                         -- Thm 2 and Lemma 4
-
-}
diff --git a/examples/logic/TheoryEng.gf b/examples/logic/TheoryEng.gf
deleted file mode 100644
index a45bc0fdd..000000000
--- a/examples/logic/TheoryEng.gf
+++ /dev/null
@@ -1,10 +0,0 @@
---# -path=.:mathematical:present:resource-1.0/api:prelude
-
-concrete TheoryEng of Theory = TheoryI with
-  (LexTheory = LexTheoryEng), 
-  (Grammar = GrammarEng), 
-  (Symbolic = SymbolicEng), 
-  (Symbol = SymbolEng), 
-  (Combinators = CombinatorsEng), 
-  (Constructors = ConstructorsEng), 
-  ;
\ No newline at end of file
diff --git a/examples/logic/TheoryI.gf b/examples/logic/TheoryI.gf
deleted file mode 100644
index 9ab457536..000000000
--- a/examples/logic/TheoryI.gf
+++ /dev/null
@@ -1,56 +0,0 @@
-incomplete concrete TheoryI of Theory = 
-  open 
-    LexTheory,
-    Grammar, 
-    Symbolic, 
-    Symbol,
-    Combinators, 
-    Constructors, 
-    (C=ConstructX),
-    Prelude 
-  in {
-
-lincat
-  Chapter = Text ;
-  Jment   = Text ;
-  Decl    = Text ;
-  Prop    = S ;
-  Branch  = S ;
-  Proof   = Text ;
-  [Proof] = Text ;
-  Typ     = CN ;
-  Obj     = NP ;
-  Label   = NP ;
-  Adverb  = PConj ;
-  Ref     = NP ;
-  [Ref]   = [NP] ;
-  Number  = Num ;
-
-lin
-  Chap title jments = 
-    appendText (mkText (mkPhr (mkUtt title)) TEmpty) jments ;
-
-  JDefObj decl a b = 
-    appendText decl (mkUtt (mkS (pred b a))) ;
-
-  DProp p = 
-    mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS p)))) TEmpty ;
-  DTyp a ty = --- x pro a: refresh bug
-    mkText (mkPhr (mkUtt (mkImp (mkVP assume_VS (mkS (pred ty a)))))) TEmpty ;
-
-  PProp p = mkText (mkPhr p) TEmpty ;
-  PAdvProp a p = mkText (mkPhr a (mkUtt p) NoVoc) TEmpty ;
-  PDecl d = d ;
-  PBranch b ps = mkText (mkPhr b) ps ;
-
-  BCases n = 
-    mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet (mkNum n2)) case_N)) ;
-
-  ARef h = mkAdv by8means_Prep h ;
-  AHence = therefore_PConj ;
-  AAFort = C.mkPConj ["a fortiori"] ;
-
-  RLabel h = h ;
-  RMany rs = mkNP and_Conj rs ;
-
-}