src/HOL/Proofs/Extraction/Util.thy

 (*  Title:      HOL/Proofs/Extraction/Util.thy
     Author:     Stefan Berghofer, TU Muenchen
 *)
 
-section {* Auxiliary lemmas used in program extraction examples *}
+section \<open>Auxiliary lemmas used in program extraction examples\<close>
 
 theory Util
 imports "~~/src/HOL/Library/Old_Datatype"
 begin
 
-text {*
+text \<open>
 Decidability of equality on natural numbers.
-*}
+\<close>
 
 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
   apply (induct m)
   apply (case_tac n)
   apply (case_tac [3] n)
   apply (simp only: nat.simps, iprover?)+
   done
 
-text {*
+text \<open>
 Well-founded induction on natural numbers, derived using the standard
 structural induction rule.
-*}
+\<close>
 
 lemma nat_wf_ind:
   assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
   shows "P z"
 proof (rule R)

       thus ?case by (rule Suc)
     qed
   qed
 qed
 
-text {*
+text \<open>
 Bounded search for a natural number satisfying a decidable predicate.
-*}
+\<close>
 
 lemma search:
   assumes dec: "\<And>x::nat. P x \<or> \<not> P x"
   shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)"
 proof (induct y)