src/HOL/Corec_Examples/Tests/Small_Concrete.thy
changeset 62726 5b2a7caa855b
parent 62696 7325d8573fb8
child 62733 ebfc41a47641
     1.1 --- a/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Mon Mar 28 12:05:47 2016 +0200
     1.2 +++ b/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Mon Mar 28 12:05:47 2016 +0200
     1.3 @@ -6,13 +6,13 @@
     1.4  Small concrete examples.
     1.5  *)
     1.6  
     1.7 -section {* Small Concrete Examples *}
     1.8 +section \<open>Small Concrete Examples\<close>
     1.9  
    1.10  theory Small_Concrete
    1.11  imports "~~/src/HOL/Library/BNF_Corec"
    1.12  begin
    1.13  
    1.14 -subsection {* Streams of Natural Numbers *}
    1.15 +subsection \<open>Streams of Natural Numbers\<close>
    1.16  
    1.17  codatatype natstream = S (head: nat) (tail: natstream)
    1.18  
    1.19 @@ -130,7 +130,7 @@
    1.20    done
    1.21  
    1.22  
    1.23 -subsection {* Lazy Lists of Natural Numbers *}
    1.24 +subsection \<open>Lazy Lists of Natural Numbers\<close>
    1.25  
    1.26  codatatype llist = LNil | LCons nat llist
    1.27  
    1.28 @@ -150,7 +150,7 @@
    1.29    "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
    1.30  
    1.31  
    1.32 -subsection {* Coinductie Natural Numbers *}
    1.33 +subsection \<open>Coinductie Natural Numbers\<close>
    1.34  
    1.35  codatatype conat = CoZero | CoSuc conat
    1.36