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 8950 3e858b72fac9
parent 8781 d0c2bd57a9fb
child 9930 c02d48a47ed1 
--- a/src/HOL/Induct/Mutil.thy	Wed May 24 18:41:09 2000 +0200
+++ b/src/HOL/Induct/Mutil.thy	Wed May 24 18:41:49 2000 +0200
@@ -23,9 +23,6 @@
     vertl  "{(i, j), (Suc i, j)} : domino"
 
 constdefs
-  below   :: "nat => nat set"
-   "below n   == {i. i<n}"
-  
   colored  :: "nat => (nat*nat)set"
    "colored b == {(i,j). (i+j) mod #2 = b}"
isabelle