src/ZF/Bool.ML
changeset 37 cebe01deba80
parent 14 1c0926788772
child 119 0e58da397b1d
--- a/src/ZF/Bool.ML	Thu Oct 07 09:49:46 1993 +0100
+++ b/src/ZF/Bool.ML	Thu Oct 07 10:48:16 1993 +0100
@@ -20,7 +20,7 @@
 by (rtac consI1 1);
 val bool_0I = result();
 
-goalw Bool.thy bool_defs "~ 1=0";
+goalw Bool.thy bool_defs "1~=0";
 by (rtac succ_not_0 1);
 val one_not_0 = result();