recdef requires theory Recdef;
authorwenzelm
Thu Apr 22 13:04:23 1999 +0200 (1999-04-22)
changeset 6481dbf2d9b3d6c8
parent 6480 c58bc3d2ba0f
child 6482 324a4051ff7b
recdef requires theory Recdef;
src/HOL/Lex/AutoChopper1.thy
src/HOL/Lex/MaxChop.thy
src/HOL/Subst/Unify.thy
src/HOL/ex/Fib.thy
src/HOL/ex/Primrec.thy
src/HOL/ex/Recdefs.thy
     1.1 --- a/src/HOL/Lex/AutoChopper1.thy	Thu Apr 22 13:03:46 1999 +0200
     1.2 +++ b/src/HOL/Lex/AutoChopper1.thy	Thu Apr 22 13:04:23 1999 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  No proofs yet.
     1.5  *)
     1.6  
     1.7 -AutoChopper1 = DA + Chopper + WF_Rel +
     1.8 +AutoChopper1 = DA + Chopper + Recdef +
     1.9  
    1.10  consts
    1.11    acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
     2.1 --- a/src/HOL/Lex/MaxChop.thy	Thu Apr 22 13:03:46 1999 +0200
     2.2 +++ b/src/HOL/Lex/MaxChop.thy	Thu Apr 22 13:04:23 1999 +0200
     2.3 @@ -4,7 +4,7 @@
     2.4      Copyright   1998 TUM
     2.5  *)
     2.6  
     2.7 -MaxChop = MaxPrefix +
     2.8 +MaxChop = MaxPrefix + Recdef +
     2.9  
    2.10  types   'a chopper = "'a list => 'a list list * 'a list"
    2.11  
     3.1 --- a/src/HOL/Subst/Unify.thy	Thu Apr 22 13:03:46 1999 +0200
     3.2 +++ b/src/HOL/Subst/Unify.thy	Thu Apr 22 13:04:23 1999 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  Unification algorithm
     3.5  *)
     3.6  
     3.7 -Unify = Unifier + WF_Rel + Option + 
     3.8 +Unify = Unifier + Recdef + Option +
     3.9  
    3.10  consts
    3.11  
     4.1 --- a/src/HOL/ex/Fib.thy	Thu Apr 22 13:03:46 1999 +0200
     4.2 +++ b/src/HOL/ex/Fib.thy	Thu Apr 22 13:04:23 1999 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  The Fibonacci function.  Demonstrates the use of recdef.
     4.5  *)
     4.6  
     4.7 -Fib = WF_Rel + Divides + Primes +
     4.8 +Fib = Divides + Primes +
     4.9  
    4.10  consts fib  :: "nat => nat"
    4.11  recdef fib "less_than"
     5.1 --- a/src/HOL/ex/Primrec.thy	Thu Apr 22 13:03:46 1999 +0200
     5.2 +++ b/src/HOL/ex/Primrec.thy	Thu Apr 22 13:04:23 1999 +0200
     5.3 @@ -16,7 +16,7 @@
     5.4  Demonstrates recursive definitions, the TFL package
     5.5  *)
     5.6  
     5.7 -Primrec = WF_Rel + List +
     5.8 +Primrec = Main +
     5.9  
    5.10  consts ack  :: "nat * nat => nat"
    5.11  recdef ack "less_than ** less_than"
     6.1 --- a/src/HOL/ex/Recdefs.thy	Thu Apr 22 13:03:46 1999 +0200
     6.2 +++ b/src/HOL/ex/Recdefs.thy	Thu Apr 22 13:04:23 1999 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -(*  Title:      HOL/ex/Recdef.thy
     6.5 +(*  Title:      HOL/ex/Recdefs.thy
     6.6      ID:         $Id$
     6.7      Author:     Konrad Slind and Lawrence C Paulson
     6.8      Copyright   1996  University of Cambridge
     6.9 @@ -95,7 +95,7 @@
    6.10  *)
    6.11  consts mapf :: nat => nat list
    6.12  recdef mapf "measure(%m. m)"
    6.13 -congs "[map_cong]"
    6.14 +congs map_cong
    6.15  "mapf 0 = []"
    6.16  "mapf (Suc n) = concat(map (%x. mapf x) (replicate n n))"
    6.17