# HG changeset patch
# User blanchet
# Date 1390238696 -3600
# Node ID 4e5ddf3162ac2cc09337c0b131c057feddec2062
# Parent  6d0af3c108648c7e2810f1fcefd7804dde69436c
tuning

diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -24,11 +24,11 @@
 definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"
 
 lemma finite_cont[simp]: "finite (cont tr)"
-  unfolding cont_def o_apply by (cases tr, clarsimp)
+  unfolding cont_def comp_apply by (cases tr, clarsimp)
 
 lemma Node_root_cont[simp]:
   "Node (root tr) (cont tr) = tr"
-  unfolding Node_def cont_def o_apply
+  unfolding Node_def cont_def comp_apply
   apply (rule trans[OF _ dtree.collapse])
   apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]])
   apply (simp_all add: fset_inject)
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy
--- a/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Derivation_Trees/Gram_Lang.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -480,7 +480,7 @@
 proof-
   {fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
    apply(induct rule: wf_raw_coind) apply safe
-   unfolding deftr_simps image_compose[symmetric] sum_map.comp id_o
+   unfolding deftr_simps image_compose[symmetric] sum_map.comp id_comp
    root_o_deftr sum_map.id image_id id_apply apply(rule S_P)
    unfolding inj_on_def by auto
   }
@@ -517,7 +517,7 @@
 lemma cont_hsubst_eq[simp]:
 assumes "root tr = root tr0"
 shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr0)"
-apply(subst id_o[symmetric, of id]) unfolding id_o
+apply(subst id_comp[symmetric, of id]) unfolding id_comp
 using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
 unfolding hsubst_def hsubst_c_def using assms by simp
 
@@ -529,7 +529,7 @@
 lemma cont_hsubst_neq[simp]:
 assumes "root tr \<noteq> root tr0"
 shows "cont (hsubst tr) = (id \<oplus> hsubst) ` (cont tr)"
-apply(subst id_o[symmetric, of id]) unfolding id_o
+apply(subst id_comp[symmetric, of id]) unfolding id_comp
 using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c]
 unfolding hsubst_def hsubst_c_def using assms by simp
 
@@ -960,7 +960,7 @@
 
 lemma cont_H[simp]:
 "cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
-apply(subst id_o[symmetric, of id]) unfolding sum_map.comp[symmetric]
+apply(subst id_comp[symmetric, of id]) unfolding sum_map.comp[symmetric]
 unfolding image_compose unfolding H_c_def[symmetric]
 using unfold(2)[of H_c n H_r, OF finite_H_c]
 unfolding H_def ..
@@ -989,7 +989,7 @@
        obtain tr2' where tr2: "tr2 = H (root tr2')"
        and tr2': "Inr tr2' \<in> cont (pick n1)"
        using tr2 Inr_cont_H[of n1]
-       unfolding tr1 image_def o_def using vimage_eq by auto
+       unfolding tr1 image_def comp_def using vimage_eq by auto
        have "inItr UNIV tr0 (root tr2')"
        using inItr.Base inItr.Ind n1 pick subtr_inItr tr2' by (metis iso_tuple_UNIV_I)
        thus "\<exists>n2. inItr UNIV tr0 n2 \<and> tr2 = H n2" using tr2 by blast
@@ -1005,7 +1005,7 @@
 using assms apply(cases t_tr)
   apply (metis (lifting) sum_map.simps(1))
   using pick H_def H_r_def unfold(1)
-      inItr.Base o_apply subtr_StepL subtr_inItr sum_map.simps(2)
+      inItr.Base comp_apply subtr_StepL subtr_inItr sum_map.simps(2)
   by (metis UNIV_I)
 
 lemma H_P:
@@ -1013,7 +1013,7 @@
 shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
 proof-
   have "?L = (n, (id \<oplus> root) ` cont (pick n))"
-  unfolding cont_H image_compose[symmetric] sum_map.comp id_o o_assoc
+  unfolding cont_H image_compose[symmetric] sum_map.comp id_comp comp_assoc
   unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
   by(rule root_H_root[OF n])
   moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF/Examples/Stream_Processor.thy
--- a/src/HOL/BNF/Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/Examples/Stream_Processor.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -62,7 +62,7 @@
   "out (sp o\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sub>\<nu> sp') (out sp o\<^sub>\<mu> out sp')"
 
 lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp: "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
-proof (rule ext, unfold o_apply)
+proof (rule ext, unfold comp_apply)
   fix s
   show "run\<^sub>\<nu> (sp o\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
   proof (coinduction arbitrary: sp sp' s)
@@ -95,7 +95,7 @@
   "out (sp o\<^sup>*\<^sub>\<nu> sp') = map_sp\<^sub>\<mu> id (\<lambda>(sp, sp'). sp o\<^sup>*\<^sub>\<nu> sp') (out sp o\<^sup>*\<^sub>\<mu> out sp')"
 
 lemma run\<^sub>\<nu>_sp\<^sub>\<nu>_comp2: "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') = run\<^sub>\<nu> sp o run\<^sub>\<nu> sp'"
-proof (rule ext, unfold o_apply)
+proof (rule ext, unfold comp_apply)
   fix s
   show "run\<^sub>\<nu> (sp o\<^sup>*\<^sub>\<nu> sp') s = run\<^sub>\<nu> sp (run\<^sub>\<nu> sp' s)"
   proof (coinduction arbitrary: sp sp' s)
@@ -157,16 +157,16 @@
 
 (* The strength laws for \<theta>: *)
 lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g"
-  unfolding \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
+  unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
 
 definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where
   "assl abc = ((fst abc, fst (snd abc)), snd (snd abc))"
 
 lemma \<theta>_rid: "F id fst o \<theta> = fst"
-  unfolding \<theta>_def F.map_comp F.map_id o_def id_apply convol_def fst_conv sym[OF id_def] ..
+  unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] ..
 
 lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl"
-  unfolding assl_def \<theta>_def F.map_comp o_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
+  unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
 
 datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
 codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF/More_BNFs.thy
--- a/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/More_BNFs.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -17,6 +17,16 @@
   "~~/src/HOL/Library/Multiset"
 begin
 
+notation
+  ordLeq2 (infix "<=o" 50) and
+  ordLeq3 (infix "\<le>o" 50) and
+  ordLess2 (infix "<o" 50) and
+  ordIso2 (infix "=o" 50) and
+  csum (infixr "+c" 65) and
+  cprod (infixr "*c" 80) and
+  cexp (infixr "^c" 90) and
+  convol ("<_ , _>")
+
 lemma option_rec_conv_option_case: "option_rec = option_case"
 by (simp add: fun_eq_iff split: option.split)
 
@@ -84,7 +94,7 @@
   thus "map f x = map g x" by simp
 next
   fix f
-  show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
+  show "set o map f = image f o set" by (rule ext, unfold comp_apply, rule set_map)
 next
   show "card_order natLeq" by (rule natLeq_card_order)
 next
@@ -237,7 +247,7 @@
   also have "... = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" unfolding comp_def ..
   finally have "setsum (count f) ?A = setsum (\<lambda> b. setsum (count f) (?As b)) ?B" .
   thus "count (mmap (h2 \<circ> h1) f) c = count ((mmap h2 \<circ> mmap h1) f) c"
-    by transfer (unfold o_apply, blast)
+    by transfer (unfold comp_apply, blast)
 qed
 
 lemma mmap_cong:
@@ -255,7 +265,7 @@
 end
 
 lemma set_of_mmap: "set_of o mmap h = image h o set_of"
-proof (rule ext, unfold o_apply)
+proof (rule ext, unfold comp_apply)
   fix M show "set_of (mmap h M) = h ` set_of M"
     by transfer (auto simp add: multiset_def setsum_gt_0_iff)
 qed
@@ -687,7 +697,7 @@
         case True
         def c \<equiv> "f1 b1"
         have c: "c \<in> set_of P" and b1: "b1 \<in> set1 c"
-          unfolding set1_def c_def P1 using True by (auto simp: o_eq_dest[OF set_of_mmap])
+          unfolding set1_def c_def P1 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
         with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p1 a = b1 \<and> a \<in> SET}"
           by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
         also have "... = setsum (count M) ((\<lambda> b2. u c b1 b2) ` (set2 c))"
@@ -723,7 +733,7 @@
         case True
         def c \<equiv> "f2 b2"
         have c: "c \<in> set_of P" and b2: "b2 \<in> set2 c"
-          unfolding set2_def c_def P2 using True by (auto simp: o_eq_dest[OF set_of_mmap])
+          unfolding set2_def c_def P2 using True by (auto simp: comp_eq_dest[OF set_of_mmap])
         with sM(1) have "setsum (count M) ?K = setsum (count M) {a. p2 a = b2 \<and> a \<in> SET}"
           by transfer (force intro: setsum_mono_zero_cong_left split: split_if_asm)
         also have "... = setsum (count M) ((\<lambda> b1. u c b1 b2) ` (set1 c))"
@@ -738,7 +748,7 @@
           apply(rule setsum_reindex)
           using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
         also have "... = setsum (\<lambda> b1. count M (u c b1 b2)) (set1 c)" by simp
-        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] o_def
+        also have "... = count N2 b2" unfolding ss2[OF c b2, symmetric] comp_def
           apply(rule setsum_cong[OF refl]) apply (transfer fixing: Ms u c b2 set1)
           using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2] set1_def by fastforce
         finally show ?thesis .
@@ -762,7 +772,7 @@
     by (blast dest: wppull_thePull)
   then show ?thesis
     by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
-      (auto simp: o_eq_dest_lhs[OF mmap_comp[symmetric]] o_eq_dest[OF set_of_mmap]
+      (auto simp: comp_eq_dest_lhs[OF mmap_comp[symmetric]] comp_eq_dest[OF set_of_mmap]
         intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
 qed
 
@@ -774,7 +784,7 @@
 by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
   Grp_def relcompp.simps intro: mmap_cong)
   (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
-    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def o_def, simplified])
+    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def comp_def, simplified])
 
 inductive rel_multiset' where
   Zero[intro]: "rel_multiset' R {#} {#}"
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -15,10 +15,10 @@
 by (rule ext) simp
 
 lemma Union_natural: "Union o image (image f) = image f o Union"
-by (rule ext) (auto simp only: o_apply)
+by (rule ext) (auto simp only: comp_apply)
 
 lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
-by (unfold o_assoc)
+by (unfold comp_assoc)
 
 lemma comp_single_set_bd:
   assumes fbd_Card_order: "Card_order fbd" and
@@ -58,7 +58,7 @@
 by blast
 
 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
-by (unfold o_apply collect_def SUP_def)
+by (unfold comp_apply collect_def SUP_def)
 
 lemma wpull_cong:
 "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -16,8 +16,8 @@
   "bnf" :: thy_goal
 begin
 
-lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
-  by (rule ext) (auto simp only: o_apply collect_def)
+lemma collect_comp: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
+  by (rule ext) (auto simp only: comp_apply collect_def)
 
 definition convol ("<_ , _>") where
 "<f , g> \<equiv> %a. (f a, g a)"
@@ -67,10 +67,10 @@
 unfolding Grp_def by auto
 
 lemma Collect_split_Grp_eqD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> (f \<circ> fst) z = snd z"
-unfolding Grp_def o_def by auto
+unfolding Grp_def comp_def by auto
 
 lemma Collect_split_Grp_inD: "z \<in> Collect (split (Grp A f)) \<Longrightarrow> fst z \<in> A"
-unfolding Grp_def o_def by auto
+unfolding Grp_def comp_def by auto
 
 definition "pick_middlep P Q a c = (SOME b. P a b \<and> Q b c)"
 
@@ -153,10 +153,6 @@
 lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
   unfolding vimage2p_def Grp_def by auto
 
-(*FIXME: duplicates lemma from Record.thy*)
-lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
-  by clarsimp
-
 ML_file "Tools/BNF/bnf_def_tactics.ML"
 ML_file "Tools/BNF/bnf_def.ML"
 
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -35,7 +35,7 @@
 by auto
 
 lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
-unfolding o_def fun_eq_iff by simp
+unfolding comp_def fun_eq_iff by simp
 
 lemma o_bij:
   assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
@@ -113,16 +113,16 @@
 by blast
 
 lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
-  unfolding o_def fun_eq_iff by auto
+  unfolding comp_def fun_eq_iff by auto
 
 lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
-  unfolding o_def fun_eq_iff by auto
+  unfolding comp_def fun_eq_iff by auto
 
 lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
-  unfolding o_def fun_eq_iff by auto
+  unfolding comp_def fun_eq_iff by auto
 
 lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
-  unfolding o_def fun_eq_iff by auto
+  unfolding comp_def fun_eq_iff by auto
 
 lemma convol_o: "<f, g> o h = <f o h, g o h>"
   unfolding convol_def by auto
@@ -131,16 +131,16 @@
   unfolding convol_def by auto
 
 lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
-  unfolding map_pair_o_convol id_o o_id ..
+  unfolding map_pair_o_convol id_comp comp_id ..
 
 lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
-  unfolding o_def by (auto split: sum.splits)
+  unfolding comp_def by (auto split: sum.splits)
 
 lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
-  unfolding o_def by (auto split: sum.splits)
+  unfolding comp_def by (auto split: sum.splits)
 
 lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
-  unfolding sum_case_o_sum_map id_o o_id ..
+  unfolding sum_case_o_sum_map id_comp comp_id ..
 
 lemma fun_rel_def_butlast:
   "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_LFP.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -225,10 +225,10 @@
 by (rule `(\<And>x y. PROP P x y)`)
 
 lemma nchotomy_relcomppE:
-  "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; (\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
+  "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; \<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by (metis relcompp.cases)
 
-lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
+lemma vimage2p_fun_rel: "fun_rel (vimage2p f g R) R f g"
   unfolding fun_rel_def vimage2p_def by auto
 
 lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/BNF_Util.thy
--- a/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF_Util.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -22,7 +22,7 @@
 lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
 by simp
 
-lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
+lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
 unfolding bij_def inj_on_def by auto blast
 
 (* Operator: *)
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/Cardinals/Cardinal_Arithmetic.thy
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,10 +11,7 @@
 imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation
 begin
 
-notation ordLeq2 (infix "<=o" 50) and
-  ordLeq3 (infix "\<le>o" 50) and
-  ordLess2 (infix "<o" 50) and
-  ordIso2 (infix "=o" 50) and
+notation
   csum (infixr "+c" 65) and
   cprod (infixr "*c" 80) and
   cexp (infixr "^c" 90)
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/Cardinals/Constructions_on_Wellorders.thy
--- a/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Constructions_on_Wellorders.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,8 @@
 imports BNF_Constructions_on_Wellorders Wellorder_Embedding Order_Union
 begin
 
-notation ordLeq2 (infix "<=o" 50) and
+notation
+  ordLeq2 (infix "<=o" 50) and
   ordLeq3 (infix "\<le>o" 50) and
   ordLess2 (infix "<o" 50) and
   ordIso2 (infix "=o" 50)
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/Cardinals/Fun_More.thy
--- a/src/HOL/Cardinals/Fun_More.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Fun_More.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,6 @@
 imports Main
 begin
 
-
 subsection {* Purely functional properties  *}
 
 (* unused *)
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/Cardinals/Order_Relation_More.thy
--- a/src/HOL/Cardinals/Order_Relation_More.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Order_Relation_More.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,6 @@
 imports Main
 begin
 
-
 subsection {* The upper and lower bounds operators  *}
 
 lemma aboveS_subset_above: "aboveS r a \<le> above r a"
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/Cardinals/Wellfounded_More.thy
--- a/src/HOL/Cardinals/Wellfounded_More.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Wellfounded_More.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,6 @@
 imports Wellfounded Order_Relation_More
 begin
 
-
 subsection {* Well-founded recursion via genuine fixpoints *}
 
 (*2*)lemma adm_wf_unique_fixpoint:
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/Cardinals/Wellorder_Embedding.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Cardinals/Wellorder_Embedding.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,7 +11,6 @@
 imports BNF_Wellorder_Embedding Fun_More Wellorder_Relation
 begin
 
-
 subsection {* Auxiliaries *}
 
 lemma UNION_bij_betw_ofilter:
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Fun.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -65,6 +65,12 @@
   "a o b = c o d \<Longrightarrow> ((\<And>v. a (b v) = c (d v)) \<Longrightarrow> R) \<Longrightarrow> R"
   by (simp add: fun_eq_iff) 
 
+lemma comp_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
+  by clarsimp
+
+lemma comp_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
+  by clarsimp
+
 lemma image_comp:
   "(f o g) ` r = f ` (g ` r)"
   by auto
@@ -915,6 +921,8 @@
 lemmas o_id = comp_id
 lemmas o_eq_dest = comp_eq_dest
 lemmas o_eq_elim = comp_eq_elim
+lemmas o_eq_dest_lhs = comp_eq_dest_lhs
+lemmas o_eq_id_dest = comp_eq_id_dest
 lemmas image_compose = image_comp
 lemmas vimage_compose = vimage_comp
 
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -24,7 +24,8 @@
   ordIso2 (infix "=o" 50) and
   csum (infixr "+c" 65) and
   cprod (infixr "*c" 80) and
-  cexp (infixr "^c" 90)
+  cexp (infixr "^c" 90) and
+  convol ("<_ , _>")
 
 no_syntax (xsymbols)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
diff -r 6d0af3c10864 -r 4e5ddf3162ac src/HOL/Record.thy
--- a/src/HOL/Record.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Record.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -411,12 +411,6 @@
 lemma K_record_comp: "(\<lambda>x. c) \<circ> f = (\<lambda>x. c)"
   by (simp add: comp_def)
 
-lemma o_eq_dest_lhs: "a o b = c \<Longrightarrow> a (b v) = c v"
-  by clarsimp
-
-lemma o_eq_id_dest: "a o b = id o c \<Longrightarrow> a (b v) = c v"
-  by clarsimp
-
 
 subsection {* Concrete record syntax *}