diff -r c09598a97436 -r d8d85a8172b5 src/HOL/Fun_Def.thy
--- a/src/HOL/Fun_Def.thy	Sat Jul 18 21:44:18 2015 +0200
+++ b/src/HOL/Fun_Def.thy	Sat Jul 18 22:58:50 2015 +0200
@@ -2,14 +2,14 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-section {* Function Definitions and Termination Proofs *}
+section \<open>Function Definitions and Termination Proofs\<close>
 
 theory Fun_Def
 imports Basic_BNF_LFPs Partial_Function SAT
 keywords "function" "termination" :: thy_goal and "fun" "fun_cases" :: thy_decl
 begin
 
-subsection {* Definitions with default value *}
+subsection \<open>Definitions with default value\<close>
 
 definition
   THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
@@ -66,7 +66,7 @@
   proof
     assume "\<exists>y. G x y"
     hence "D x" using graph ..
-    with `\<not> D x` show False ..
+    with \<open>\<not> D x\<close> show False ..
   qed
   hence "\<not>(\<exists>!y. G x y)" by blast
 
@@ -88,26 +88,26 @@
 ML_file "Tools/Function/relation.ML"
 ML_file "Tools/Function/function_elims.ML"
 
-method_setup relation = {*
+method_setup relation = \<open>
   Args.term >> (fn t => fn ctxt => SIMPLE_METHOD' (Function_Relation.relation_infer_tac ctxt t))
-*} "prove termination using a user-specified wellfounded relation"
+\<close> "prove termination using a user-specified wellfounded relation"
 
 ML_file "Tools/Function/function.ML"
 ML_file "Tools/Function/pat_completeness.ML"
 
-method_setup pat_completeness = {*
+method_setup pat_completeness = \<open>
   Scan.succeed (SIMPLE_METHOD' o Pat_Completeness.pat_completeness_tac)
-*} "prove completeness of (co)datatype patterns"
+\<close> "prove completeness of (co)datatype patterns"
 
 ML_file "Tools/Function/fun.ML"
 ML_file "Tools/Function/induction_schema.ML"
 
-method_setup induction_schema = {*
+method_setup induction_schema = \<open>
   Scan.succeed (EMPTY_CASES oo Induction_Schema.induction_schema_tac)
-*} "prove an induction principle"
+\<close> "prove an induction principle"
 
 
-subsection {* Measure functions *}
+subsection \<open>Measure functions\<close>
 
 inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
 where is_measure_trivial: "is_measure f"
@@ -125,13 +125,13 @@
 
 ML_file "Tools/Function/lexicographic_order.ML"
 
-method_setup lexicographic_order = {*
+method_setup lexicographic_order = \<open>
   Method.sections clasimp_modifiers >>
   (K (SIMPLE_METHOD o Lexicographic_Order.lexicographic_order_tac false))
-*} "termination prover for lexicographic orderings"
+\<close> "termination prover for lexicographic orderings"
 
 
-subsection {* Congruence rules *}
+subsection \<open>Congruence rules\<close>
 
 lemma let_cong [fundef_cong]:
   "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
@@ -151,7 +151,7 @@
   unfolding o_apply .
 
 
-subsection {* Simp rules for termination proofs *}
+subsection \<open>Simp rules for termination proofs\<close>
 
 declare
   trans_less_add1[termination_simp]
@@ -166,7 +166,7 @@
 by (induct p) auto
 
 
-subsection {* Decomposition *}
+subsection \<open>Decomposition\<close>
 
 lemma less_by_empty:
   "A = {} \<Longrightarrow> A \<subseteq> B"
@@ -179,7 +179,7 @@
 by (auto simp add: wf_comp_self[of R])
 
 
-subsection {* Reduction pairs *}
+subsection \<open>Reduction pairs\<close>
 
 definition
   "reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
@@ -194,11 +194,11 @@
   assumes "wf S"
   shows "wf (R \<union> S)"
 proof -
-  from rp `S \<subseteq> snd P` have "wf (fst P)" "fst P O S \<subseteq> fst P"
+  from rp \<open>S \<subseteq> snd P\<close> have "wf (fst P)" "fst P O S \<subseteq> fst P"
     unfolding reduction_pair_def by auto
-  with `wf S` have "wf (fst P \<union> S)"
+  with \<open>wf S\<close> have "wf (fst P \<union> S)"
     by (auto intro: wf_union_compatible)
-  moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
+  moreover from \<open>R \<subseteq> fst P\<close> have "R \<union> S \<subseteq> fst P \<union> S" by auto
   ultimately show ?thesis by (rule wf_subset)
 qed
 
@@ -211,7 +211,7 @@
   by force
 
 
-subsection {* Concrete orders for SCNP termination proofs *}
+subsection \<open>Concrete orders for SCNP termination proofs\<close>
 
 definition "pair_less = less_than <*lex*> less_than"
 definition "pair_leq = pair_less^="
@@ -223,14 +223,14 @@
 lemma wf_pair_less[simp]: "wf pair_less"
   by (auto simp: pair_less_def)
 
-text {* Introduction rules for @{text pair_less}/@{text pair_leq} *}
+text \<open>Introduction rules for @{text pair_less}/@{text pair_leq}\<close>
 lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
   and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
   unfolding pair_leq_def pair_less_def by auto
 
-text {* Introduction rules for max *}
+text \<open>Introduction rules for max\<close>
 lemma smax_emptyI:
   "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict"
   and smax_insertI:
@@ -241,7 +241,7 @@
   "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak"
 unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
 
-text {* Introduction rules for min *}
+text \<open>Introduction rules for min\<close>
 lemma smin_emptyI:
   "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict"
   and smin_insertI:
@@ -252,7 +252,7 @@
   "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak"
 by (auto simp: min_strict_def min_weak_def min_ext_def)
 
-text {* Reduction Pairs *}
+text \<open>Reduction Pairs\<close>
 
 lemma max_ext_compat:
   assumes "R O S \<subseteq> R"
@@ -294,7 +294,7 @@
 by (auto simp: pair_less_def pair_leq_def)
 
 
-subsection {* Tool setup *}
+subsection \<open>Tool setup\<close>
 
 ML_file "Tools/Function/termination.ML"
 ML_file "Tools/Function/scnp_solve.ML"
@@ -302,9 +302,9 @@
 ML_file "Tools/Function/fun_cases.ML"
 
 ML_val -- "setup inactive"
-{*
+\<open>
   Context.theory_map (Function_Common.set_termination_prover
     (K (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])))
-*}
+\<close>
 
 end