--- a/src/HOL/Induct/Mutil.thy Fri Jun 06 10:46:26 1997 +0200
+++ b/src/HOL/Induct/Mutil.thy Fri Jun 06 10:47:16 1997 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/ex/Mutil
+(* Title: HOL/Induct/Mutil
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
@@ -11,8 +11,8 @@
Mutil = Finite +
consts
domino :: "(nat*nat)set set"
- tiling :: 'a set set => 'a set set
- below :: nat => nat set
+ tiling :: "'a set set => 'a set set"
+ below :: "nat => nat set"
evnodd :: "[(nat*nat)set, nat] => (nat*nat)set"
inductive domino
@@ -26,7 +26,7 @@
Un "[| a: A; t: tiling A; a <= Compl t |] ==> a Un t : tiling A"
defs
- below_def "below n == nat_rec {} insert n"
+ below_def "below n == {i. i<n}"
evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
end