Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Induct/Mutil.thy
changeset 5931 325300576da7
parent 3424 bf466159ef84
child 8340 c169cd21fe42 
--- a/src/HOL/Induct/Mutil.thy	Wed Nov 18 11:12:29 1998 +0100
+++ b/src/HOL/Induct/Mutil.thy	Wed Nov 18 15:10:46 1998 +0100
@@ -23,7 +23,7 @@
 inductive "tiling A"
   intrs
     empty  "{} : tiling A"
-    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
+    Un     "[| a: A;  t: tiling A;  a <= -t |] ==> a Un t : tiling A"
 
 defs
   below_def  "below n    == {i. i<n}"
isabelle