src/HOL/ex/Mutil.thy

--- a/src/HOL/ex/Mutil.thy	Fri Jun 21 13:51:09 1996 +0200
+++ b/src/HOL/ex/Mutil.thy	Tue Jun 25 13:11:29 1996 +0200
@@ -26,7 +26,7 @@
     Un     "[| a: A;  t: tiling A;  a Int t = {} |] ==> a Un t : tiling A"
 
 defs
-  below_def  "below n    == nat_rec n {} insert"
+  below_def  "below n    == nat_rec {} insert n"
   evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
 
 end