X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Ftoolbox.ma;h=adc6b1d83650d13ae19febc219ec1e805e9cc960;hb=070b44c9c2344967ca8c4531909614a0d4da2fbe;hp=2b076ee7f970bbe672e36bee7f3d1434cf6cfa71;hpb=4cff1c91c102e84fa930383633efe16492264051;p=helm.git

diff --git a/helm/software/matita/library/demo/toolbox.ma b/helm/software/matita/library/demo/toolbox.ma
index 2b076ee7f..adc6b1d83 100644
--- 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
+*)