--- 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"
--- 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"
--- 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): *)