src/HOL/Induct/Tree.thy

 (*  Title:      HOL/Induct/Tree.thy
     Author:     Stefan Berghofer,  TU Muenchen
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 *)
 
-section {* Infinitely branching trees *}
+section \<open>Infinitely branching trees\<close>
 
 theory Tree
 imports Main
 begin
 

   "(!!x. P x ==> Q (f x)) ==>
     exists_tree P ts ==> exists_tree Q (map_tree f ts)"
   by (induct ts) auto
 
 
-subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
+subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close>
 
 datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
 
-text{*Addition of ordinals*}
+text\<open>Addition of ordinals\<close>
 primrec add :: "[brouwer,brouwer] => brouwer"
 where
   "add i Zero = i"
 | "add i (Succ j) = Succ (add i j)"
 | "add i (Lim f) = Lim (%n. add i (f n))"
 
 lemma add_assoc: "add (add i j) k = add i (add j k)"
   by (induct k) auto
 
-text{*Multiplication of ordinals*}
+text\<open>Multiplication of ordinals\<close>
 primrec mult :: "[brouwer,brouwer] => brouwer"
 where
   "mult i Zero = Zero"
 | "mult i (Succ j) = add (mult i j) i"
 | "mult i (Lim f) = Lim (%n. mult i (f n))"

   by (induct k) (auto simp add: add_assoc)
 
 lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
   by (induct k) (auto simp add: add_mult_distrib)
 
-text{*We could probably instantiate some axiomatic type classes and use
-the standard infix operators.*}
+text\<open>We could probably instantiate some axiomatic type classes and use
+the standard infix operators.\<close>
 
-subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*}
+subsection\<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close>
 
-text{*To use the function package we need an ordering on the Brouwer
+text\<open>To use the function package we need an ordering on the Brouwer
   ordinals.  Start with a predecessor relation and form its transitive 
-  closure. *} 
+  closure.\<close> 
 
 definition brouwer_pred :: "(brouwer * brouwer) set"
   where "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
 
 definition brouwer_order :: "(brouwer * brouwer) set"

   by(auto simp add: brouwer_order_def brouwer_pred_def)
 
 lemma [simp]: "(f n, Lim f) : brouwer_order"
   by(auto simp add: brouwer_order_def brouwer_pred_def)
 
-text{*Example of a general function*}
+text\<open>Example of a general function\<close>
 
 function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
 where
   "add2 i Zero = i"
 | "add2 i (Succ j) = Succ (add2 i j)"