- init_cache_and_tables rewritten using the automation_cache

[helm.git] / helm / software / matita / library / demo / toolbox.ma

diff --git a/helm/software/matita/library/demo/toolbox.ma b/helm/software/matita/library/demo/toolbox.ma
index 2b076ee7f970bbe672e36bee7f3d1434cf6cfa71..adc6b1d83650d13ae19febc219ec1e805e9cc960 100644 (file)
--- a/helm/software/matita/library/demo/toolbox.ma
+++ b/helm/software/matita/library/demo/toolbox.ma
@@ -48,7 +48,6 @@ definition proofs: CProp → setoid.
  constructor 1;
   [ apply A
   | intros;
-    alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
     apply True
   | intro;
     constructor 1
@@ -71,7 +70,6 @@ definition proofs1: CProp → setoid1.
  constructor 1;
   [ apply A
   | intros;
-    alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
     apply True
   | intro;
     constructor 1
@@ -259,4 +257,4 @@ definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A.
      |
   |
   |
-*)
\ No newline at end of file
+*)