src/HOL/Proofs/ex/Hilbert_Classical.thy

 (*  Title:      HOL/Proofs/ex/Hilbert_Classical.thy
     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
 *)
 
-section {* Hilbert's choice and classical logic *}
+section \<open>Hilbert's choice and classical logic\<close>
 
 theory Hilbert_Classical
 imports Main
 begin
 
-text {*
+text \<open>
   Derivation of the classical law of tertium-non-datur by means of
   Hilbert's choice operator (due to M. J. Beeson and J. Harrison).
-*}
+\<close>
 
 
-subsection {* Proof text *}
+subsection \<open>Proof text\<close>
 
 theorem tnd: "A \<or> \<not> A"
 proof -
   let ?P = "\<lambda>X. X = False \<or> X = True \<and> A"
   let ?Q = "\<lambda>X. X = False \<and> A \<or> X = True"

     qed
   qed
 qed
 
 
-subsection {* Proof term of text *}
+subsection \<open>Proof term of text\<close>
 
 prf tnd
 
 
-subsection {* Proof script *}
+subsection \<open>Proof script\<close>
 
 theorem tnd': "A \<or> \<not> A"
   apply (subgoal_tac
     "(((SOME x. x = False \<or> x = True \<and> A) = False) \<or>
       ((SOME x. x = False \<or> x = True \<and> A) = True) \<and> A) \<and>

   apply (erule conjI)
   apply assumption
   done
 
 
-subsection {* Proof term of script *}
+subsection \<open>Proof term of script\<close>
 
 prf tnd'
 
 end