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

1 files changed, 0 insertions, 59 deletions

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 ;
-
-}