src/HOL/Library/Old_Recdef.thy
changeset 58881 b9556a055632
parent 58825 2065f49da190
child 60500 903bb1495239
equal deleted inserted replaced
58880:0baae4311a9f 58881:b9556a055632
     1 (*  Title:      HOL/Library/Old_Recdef.thy
     1 (*  Title:      HOL/Library/Old_Recdef.thy
     2     Author:     Konrad Slind and Markus Wenzel, TU Muenchen
     2     Author:     Konrad Slind and Markus Wenzel, TU Muenchen
     3 *)
     3 *)
     4 
     4 
     5 header {* TFL: recursive function definitions *}
     5 section {* TFL: recursive function definitions *}
     6 
     6 
     7 theory Old_Recdef
     7 theory Old_Recdef
     8 imports Main
     8 imports Main
     9 keywords
     9 keywords
    10   "recdef" "defer_recdef" :: thy_decl and
    10   "recdef" "defer_recdef" :: thy_decl and