src/HOL/Library/Old_Recdef.thy
changeset 55017 2df6ad1dbd66
parent 48891 c0eafbd55de3
child 56248 67dc9549fa15
equal deleted inserted replaced
55016:9fc7e7753d86 55017:2df6ad1dbd66
     3 *)
     3 *)
     4 
     4 
     5 header {* TFL: recursive function definitions *}
     5 header {* TFL: recursive function definitions *}
     6 
     6 
     7 theory Old_Recdef
     7 theory Old_Recdef
     8 imports Wfrec
     8 imports Main
     9 keywords
     9 keywords
    10   "recdef" "defer_recdef" :: thy_decl and
    10   "recdef" "defer_recdef" :: thy_decl and
    11   "recdef_tc" :: thy_goal and
    11   "recdef_tc" :: thy_goal and
    12   "permissive" "congs" "hints"
    12   "permissive" "congs" "hints"
    13 begin
    13 begin