# HG changeset patch
# User wenzelm
# Date 924779063 -7200
# Node ID dbf2d9b3d6c86f861a29cf25612bcfeba829910c
# Parent  c58bc3d2ba0f17130ef5525059477a9aed030308
recdef requires theory Recdef;

diff -r c58bc3d2ba0f -r dbf2d9b3d6c8 src/HOL/Lex/AutoChopper1.thy
--- 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)
diff -r c58bc3d2ba0f -r dbf2d9b3d6c8 src/HOL/Lex/MaxChop.thy
--- 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"
 
diff -r c58bc3d2ba0f -r dbf2d9b3d6c8 src/HOL/Subst/Unify.thy
--- 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
 
diff -r c58bc3d2ba0f -r dbf2d9b3d6c8 src/HOL/ex/Fib.thy
--- 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"
diff -r c58bc3d2ba0f -r dbf2d9b3d6c8 src/HOL/ex/Primrec.thy
--- 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"
diff -r c58bc3d2ba0f -r dbf2d9b3d6c8 src/HOL/ex/Recdefs.thy
--- 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))"