diff -r 3684a4420a67 -r bf466159ef84 src/HOL/Induct/Mutil.thy
--- 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