# HG changeset patch
# User blanchet
# Date 1459159547 -7200
# Node ID 5b2a7caa855b6c0354235619ce897653d2122b34
# Parent  5ab1746186c77be5ceaa9c9bfe16c2c123084e7a
tuned examples

diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/LFilter.thy
--- a/src/HOL/Corec_Examples/LFilter.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/LFilter.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -7,7 +7,7 @@
 The filter function on lazy lists.
 *)
 
-section {* The Filter Function on Lazy Lists *}
+section \<open>The Filter Function on Lazy Lists\<close>
 
 theory LFilter
 imports "~~/src/HOL/Library/BNF_Corec"
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Stream_Processor.thy
--- a/src/HOL/Corec_Examples/Stream_Processor.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Stream_Processor.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -7,7 +7,7 @@
 Stream processors---a syntactic representation of continuous functions on streams.
 *)
 
-section {* Stream Processors---A Syntactic Representation of Continuous Functions on Streams *}
+section \<open>Stream Processors---A Syntactic Representation of Continuous Functions on Streams\<close>
 
 theory Stream_Processor
 imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream"
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy
--- a/src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/GPV_Bare_Bones.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,7 +6,7 @@
 A bare bones version of generative probabilistic values (GPVs).
 *)
 
-section {* A Bare Bones Version of Generative Probabilistic Values (GPVs) *}
+section \<open>A Bare Bones Version of Generative Probabilistic Values (GPVs)\<close>
 
 theory GPV_Bare_Bones
 imports "~~/src/HOL/Library/BNF_Corec"
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Merge_A.thy
--- a/src/HOL/Corec_Examples/Tests/Merge_A.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Merge_A.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,7 +6,7 @@
 Tests theory merges.
 *)
 
-section {* Tests Theory Merges *}
+section \<open>Tests Theory Merges\<close>
 
 theory Merge_A
 imports "~~/src/HOL/Library/BNF_Corec"
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Merge_B.thy
--- a/src/HOL/Corec_Examples/Tests/Merge_B.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Merge_B.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,7 +6,7 @@
 Tests theory merges.
 *)
 
-section {* Tests Theory Merges *}
+section \<open>Tests Theory Merges\<close>
 
 theory Merge_B
 imports Merge_A
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Merge_C.thy
--- a/src/HOL/Corec_Examples/Tests/Merge_C.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Merge_C.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,7 +6,7 @@
 Tests theory merges.
 *)
 
-section {* Tests Theory Merges *}
+section \<open>Tests Theory Merges\<close>
 
 theory Merge_C
 imports Merge_A
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Merge_D.thy
--- a/src/HOL/Corec_Examples/Tests/Merge_D.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Merge_D.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,7 +6,7 @@
 Tests theory merges.
 *)
 
-section {* Tests Theory Merges *}
+section \<open>Tests Theory Merges\<close>
 
 theory Merge_D
 imports Merge_B Merge_C
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Merge_Poly.thy
--- a/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Merge_Poly.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,13 +6,13 @@
 Tests polymorphic merges.
 *)
 
-section {* Tests Polymorphic Merges *}
+section \<open>Tests Polymorphic Merges\<close>
 
 theory Merge_Poly
 imports "~~/src/HOL/Library/BNF_Corec"
 begin
 
-subsection {* A Monomorphic Example *}
+subsection \<open>A Monomorphic Example\<close>
 
 codatatype r = R (rhd: nat) (rtl: r)
 
@@ -46,7 +46,7 @@
   "id_rx r = f1 (f2 (f3 (R (rhd r) (id_rx (rtl r)))))"
 
 
-subsection {* The Polymorphic Version *}
+subsection \<open>The Polymorphic Version\<close>
 
 codatatype 'a s = S (shd: 'a) (stl: "'a s")
 
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Misc_Mono.thy
--- a/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Misc_Mono.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,7 +6,7 @@
 Miscellaneous monomorphic examples.
 *)
 
-section {* Miscellaneous Monomorphic Examples *}
+section \<open>Miscellaneous Monomorphic Examples\<close>
 
 theory Misc_Mono
 imports "~~/src/HOL/Library/BNF_Corec"
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Misc_Poly.thy
--- a/src/HOL/Corec_Examples/Tests/Misc_Poly.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Misc_Poly.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,7 +6,7 @@
 Miscellaneous polymorphic examples.
 *)
 
-section {* Miscellaneous Polymorphic Examples *}
+section \<open>Miscellaneous Polymorphic Examples\<close>
 
 theory Misc_Poly
 imports "~~/src/HOL/Library/BNF_Corec"
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Simple_Nesting.thy
--- a/src/HOL/Corec_Examples/Tests/Simple_Nesting.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Simple_Nesting.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,13 +6,13 @@
 Tests "corec"'s parsing of map functions.
 *)
 
-section {* Tests "corec"'s Parsing of Map Functions *}
+section \<open>Tests "corec"'s Parsing of Map Functions\<close>
 
 theory Simple_Nesting
 imports "~~/src/HOL/Library/BNF_Corec"
 begin
 
-subsection {* Corecursion via Map Functions *}
+subsection \<open>Corecursion via Map Functions\<close>
 
 consts
   g :: 'a
@@ -59,7 +59,7 @@
     (map Inl (h x)))"
 
 
-subsection {* Constructors instead of Maps *}
+subsection \<open>Constructors instead of Maps\<close>
 
 codatatype 'a y = Y 'a "'a y list"
 
@@ -78,7 +78,7 @@
   "gg a = X a (Some (gg a))"
 
 
-subsection {* Some Friends *}
+subsection \<open>Some Friends\<close>
 
 codatatype u =
   U (lab: nat) (sub: "u list")
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/Small_Concrete.thy
--- a/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/Small_Concrete.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -6,13 +6,13 @@
 Small concrete examples.
 *)
 
-section {* Small Concrete Examples *}
+section \<open>Small Concrete Examples\<close>
 
 theory Small_Concrete
 imports "~~/src/HOL/Library/BNF_Corec"
 begin
 
-subsection {* Streams of Natural Numbers *}
+subsection \<open>Streams of Natural Numbers\<close>
 
 codatatype natstream = S (head: nat) (tail: natstream)
 
@@ -130,7 +130,7 @@
   done
 
 
-subsection {* Lazy Lists of Natural Numbers *}
+subsection \<open>Lazy Lists of Natural Numbers\<close>
 
 codatatype llist = LNil | LCons nat llist
 
@@ -150,7 +150,7 @@
   "fold_map f a s = (let v = f a (head s) in S v (fold_map f v (tail s)))"
 
 
-subsection {* Coinductie Natural Numbers *}
+subsection \<open>Coinductie Natural Numbers\<close>
 
 codatatype conat = CoZero | CoSuc conat
 
diff -r 5ab1746186c7 -r 5b2a7caa855b src/HOL/Corec_Examples/Tests/TLList_Friends.thy
--- a/src/HOL/Corec_Examples/Tests/TLList_Friends.thy	Mon Mar 28 12:05:47 2016 +0200
+++ b/src/HOL/Corec_Examples/Tests/TLList_Friends.thy	Mon Mar 28 12:05:47 2016 +0200
@@ -3,10 +3,10 @@
     Author:     Jasmin Blanchette, Inria, LORIA, MPII
     Copyright   2015, 2016
 
-Terminated lists examples
+Friendly functions on terminated lists.
 *)
 
-section {* Small Concrete Examples *}
+section \<open>Friendly Functions on Terminated Lists\<close>
 
 theory TLList_Friends
 imports "~~/src/HOL/Library/BNF_Corec"
@@ -43,7 +43,7 @@
 corec prd2 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
   "prd2 xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd2 (tltl xs) ys))"
 
-text {* Outer if: *}
+text \<open>Outer if:\<close>
 
 corec takeUntilOdd :: "(int, int) tllist \<Rightarrow> (int, int) tllist" where
   "takeUntilOdd xs =
@@ -75,7 +75,7 @@
         else TLNil y)"
         sorry
 
-text {* If inside the constructor: *}
+text \<open>If inside the constructor:\<close>
 
 corec prd3 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
   "prd3 xs ys = TLCons (tlhd xs * tlhd ys)
@@ -88,7 +88,7 @@
       else prd3 (tltl xs) (tltl ys))"
  sorry
 
-text {* If inside the inner friendly operation: *}
+text \<open>If inside the inner friendly operation:\<close>
 
 corec prd4 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
   "prd4 xs ys = TLCons (tlhd xs * tlhd ys)
@@ -99,7 +99,7 @@
      (pls (if undefined then prd xs (tltl ys) else xs) (prd (tltl xs) ys))"
   sorry
 
-text {* Lots of if's: *}
+text \<open>Lots of if's:\<close>
 
 corec iffy :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
   "iffy xs =