]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/esempi/calcolo_proposizioni.cic
This commit was manufactured by cvs2svn to create branch 'moogle'.
[helm.git] / helm / gTopLevel / esempi / calcolo_proposizioni.cic
diff --git a/helm/gTopLevel/esempi/calcolo_proposizioni.cic b/helm/gTopLevel/esempi/calcolo_proposizioni.cic
deleted file mode 100644 (file)
index a069a8b..0000000
+++ /dev/null
@@ -1,17 +0,0 @@
-alias True     /Coq/Init/Logic/True.ind#1/1
-alias I        /Coq/Init/Logic/True.ind#1/1/1
-alias True_ind /Coq/Init/Logic/True_ind.con
-
-alias False     /Coq/Init/Logic/False.ind#1/1
-alias False_ind /Coq/Init/Logic/False_ind.con
-
-alias and     /Coq/Init/Logic/and.ind#1/1
-alias conj    /Coq/Init/Logic/and.ind#1/1/1
-alias and_ind /Coq/Init/Logic/and_ind.con
-
-alias or        /Coq/Init/Logic/or.ind#1/1
-alias or_introl /Coq/Init/Logic/or.ind#1/1/1
-alias or_intror /Coq/Init/Logic/or.ind#1/1/2
-alias or_ind    /Coq/Init/Logic/or_ind.con
-
-alias not          /Coq/Init/Logic/not.con