--- a/src/HOL/Lex/AutoChopper1.thy Thu Apr 22 13:03:46 1999 +0200
+++ b/src/HOL/Lex/AutoChopper1.thy Thu Apr 22 13:04:23 1999 +0200
@@ -17,7 +17,7 @@
No proofs yet.
*)
-AutoChopper1 = DA + Chopper + WF_Rel +
+AutoChopper1 = DA + Chopper + Recdef +
consts
acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
--- a/src/HOL/Lex/MaxChop.thy Thu Apr 22 13:03:46 1999 +0200
+++ b/src/HOL/Lex/MaxChop.thy Thu Apr 22 13:04:23 1999 +0200
@@ -4,7 +4,7 @@
Copyright 1998 TUM
*)
-MaxChop = MaxPrefix +
+MaxChop = MaxPrefix + Recdef +
types 'a chopper = "'a list => 'a list list * 'a list"
--- a/src/HOL/Subst/Unify.thy Thu Apr 22 13:03:46 1999 +0200
+++ b/src/HOL/Subst/Unify.thy Thu Apr 22 13:04:23 1999 +0200
@@ -6,7 +6,7 @@
Unification algorithm
*)
-Unify = Unifier + WF_Rel + Option +
+Unify = Unifier + Recdef + Option +
consts
--- a/src/HOL/ex/Fib.thy Thu Apr 22 13:03:46 1999 +0200
+++ b/src/HOL/ex/Fib.thy Thu Apr 22 13:04:23 1999 +0200
@@ -6,7 +6,7 @@
The Fibonacci function. Demonstrates the use of recdef.
*)
-Fib = WF_Rel + Divides + Primes +
+Fib = Divides + Primes +
consts fib :: "nat => nat"
recdef fib "less_than"
--- a/src/HOL/ex/Primrec.thy Thu Apr 22 13:03:46 1999 +0200
+++ b/src/HOL/ex/Primrec.thy Thu Apr 22 13:04:23 1999 +0200
@@ -16,7 +16,7 @@
Demonstrates recursive definitions, the TFL package
*)
-Primrec = WF_Rel + List +
+Primrec = Main +
consts ack :: "nat * nat => nat"
recdef ack "less_than ** less_than"
--- a/src/HOL/ex/Recdefs.thy Thu Apr 22 13:03:46 1999 +0200
+++ b/src/HOL/ex/Recdefs.thy Thu Apr 22 13:04:23 1999 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/ex/Recdef.thy
+(* Title: HOL/ex/Recdefs.thy
ID: $Id$
Author: Konrad Slind and Lawrence C Paulson
Copyright 1996 University of Cambridge
@@ -95,7 +95,7 @@
*)
consts mapf :: nat => nat list
recdef mapf "measure(%m. m)"
-congs "[map_cong]"
+congs map_cong
"mapf 0 = []"
"mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"