src/HOL/Library/Old_Recdef.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60520 09fc5eaa21ce
     1.1 --- a/src/HOL/Library/Old_Recdef.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/Old_Recdef.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Konrad Slind and Markus Wenzel, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* TFL: recursive function definitions *}
     1.8 +section \<open>TFL: recursive function definitions\<close>
     1.9  
    1.10  theory Old_Recdef
    1.11  imports Main
    1.12 @@ -12,7 +12,7 @@
    1.13    "permissive" "congs" "hints"
    1.14  begin
    1.15  
    1.16 -subsection {* Lemmas for TFL *}
    1.17 +subsection \<open>Lemmas for TFL\<close>
    1.18  
    1.19  lemma tfl_wf_induct: "ALL R. wf R -->  
    1.20         (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
    1.21 @@ -70,7 +70,7 @@
    1.22  ML_file "~~/src/HOL/Tools/recdef.ML"
    1.23  
    1.24  
    1.25 -subsection {* Rule setup *}
    1.26 +subsection \<open>Rule setup\<close>
    1.27  
    1.28  lemmas [recdef_simp] =
    1.29    inv_image_def