equal
deleted
inserted
replaced
9 |
9 |
10 theory Prelim |
10 theory Prelim |
11 imports "~~/src/HOL/Library/FSet" |
11 imports "~~/src/HOL/Library/FSet" |
12 begin |
12 begin |
13 |
13 |
14 notation BNF_Def.convol ("<_ , _>") |
14 notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>") |
15 |
15 |
16 declare fset_to_fset[simp] |
16 declare fset_to_fset[simp] |
17 |
17 |
18 lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s" |
18 lemma fst_snd_convol_o[simp]: "\<langle>fst o s, snd o s\<rangle> = s" |
19 apply(rule ext) by (simp add: convol_def) |
19 apply(rule ext) by (simp add: convol_def) |
20 |
20 |
21 abbreviation sm_abbrev (infix "\<oplus>" 60) |
21 abbreviation sm_abbrev (infix "\<oplus>" 60) |
22 where "f \<oplus> g \<equiv> Sum_Type.map_sum f g" |
22 where "f \<oplus> g \<equiv> Sum_Type.map_sum f g" |
23 |
23 |