--- a/src/HOL/Library/Old_Recdef.thy Wed Jun 17 10:57:11 2015 +0200
+++ b/src/HOL/Library/Old_Recdef.thy Wed Jun 17 11:03:05 2015 +0200
@@ -2,7 +2,7 @@
Author: Konrad Slind and Markus Wenzel, TU Muenchen
*)
-section {* TFL: recursive function definitions *}
+section \<open>TFL: recursive function definitions\<close>
theory Old_Recdef
imports Main
@@ -12,7 +12,7 @@
"permissive" "congs" "hints"
begin
-subsection {* Lemmas for TFL *}
+subsection \<open>Lemmas for TFL\<close>
lemma tfl_wf_induct: "ALL R. wf R -->
(ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
@@ -70,7 +70,7 @@
ML_file "~~/src/HOL/Tools/recdef.ML"
-subsection {* Rule setup *}
+subsection \<open>Rule setup\<close>
lemmas [recdef_simp] =
inv_image_def