# HG changeset patch
# User blanchet
# Date 1390263289 -3600
# Node ID c43394c2e5eca9c1881e9e813588c7f2556ea974
# Parent  9475b16e520b46d543cadafaffa5e75a05c4471c
compile

diff -r 9475b16e520b -r c43394c2e5ec src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy
--- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Mon Jan 20 23:43:42 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Tue Jan 21 01:14:49 2014 +0100
@@ -11,6 +11,8 @@
 imports "~~/src/HOL/Library/More_BNFs"
 begin
 
+notation BNF_Def.convol ("<_ , _>")
+
 declare fset_to_fset[simp]
 
 lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s"
diff -r 9475b16e520b -r c43394c2e5ec src/HOL/BNF_Examples/Stream_Processor.thy
--- a/src/HOL/BNF_Examples/Stream_Processor.thy	Mon Jan 20 23:43:42 2014 +0100
+++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Tue Jan 21 01:14:49 2014 +0100
@@ -152,8 +152,10 @@
 
 bnf_decl ('a, 'b) F (map: F)
 
+notation BNF_Def.convol ("<_ , _>")
+
 definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where
-   "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
+  "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
 
 (* The strength laws for \<theta>: *)
 lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g"
diff -r 9475b16e520b -r c43394c2e5ec src/HOL/BNF_Examples/TreeFsetI.thy
--- a/src/HOL/BNF_Examples/TreeFsetI.thy	Mon Jan 20 23:43:42 2014 +0100
+++ b/src/HOL/BNF_Examples/TreeFsetI.thy	Tue Jan 21 01:14:49 2014 +0100
@@ -12,8 +12,6 @@
 imports "~~/src/HOL/Library/More_BNFs"
 begin
 
-hide_fact (open) Lifting_Product.prod_rel_def
-
 codatatype 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
 
 (* tree map (contrived example): *)