--- 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"
--- 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"
--- 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"
--- 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"
--- 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
--- 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
--- 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
--- 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")
--- 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"
--- 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"
--- 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")
--- 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
--- 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 =