author paulson Tue, 20 Apr 1999 14:36:19 +0200 changeset 6455 34c6c2944908 parent 6454 1c8f48966033 child 6456 23602e214ebf
Main is the correct parent
 src/HOL/ex/Primes.thy file | annotate | diff | comparison | revisions src/HOL/ex/Recdefs.thy file | annotate | diff | comparison | revisions
```--- 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```
```--- 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"```