# HG changeset patch
# User paulson
# Date 924611779 -7200
# Node ID 34c6c2944908edb316f75956698a34a20c42ce17
# Parent  1c8f48966033071a2f47f3113094fc3cf51a2402
Main is the correct parent

diff -r 1c8f48966033 -r 34c6c2944908 src/HOL/ex/Primes.thy
--- a/src/HOL/ex/Primes.thy	Tue Apr 20 14:35:12 1999 +0200
+++ b/src/HOL/ex/Primes.thy	Tue Apr 20 14:36:19 1999 +0200
@@ -11,7 +11,7 @@
 	Isabelle prove those conditions.
 *)
 
-Primes = Divides + Recdef + Datatype +
+Primes = Main +
 consts
   is_gcd  :: [nat,nat,nat]=>bool          (*gcd as a relation*)
   gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
@@ -19,7 +19,7 @@
   prime   :: nat set
   
 recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
-(*  simpset "!simpset addsimps [mod_less_divisor, zero_less_eq]" *)
+(*  simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" *)
     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
 
 defs
diff -r 1c8f48966033 -r 34c6c2944908 src/HOL/ex/Recdefs.thy
--- a/src/HOL/ex/Recdefs.thy	Tue Apr 20 14:35:12 1999 +0200
+++ b/src/HOL/ex/Recdefs.thy	Tue Apr 20 14:36:19 1999 +0200
@@ -6,7 +6,7 @@
 Examples of recdef definitions.  Most, but not all, are handled automatically.
 *)
 
-Recdefs = Recdef + List +
+Recdefs = Main +
 
 consts fact :: "nat => nat"
 recdef fact "less_than"