equal
deleted
inserted
replaced
1 (* Title: HOL/Codatatype/Examples/Infinite_Derivation_Trees/Prelim.thy |
1 (* Title: HOL/BNF/Examples/Infinite_Derivation_Trees/Prelim.thy |
2 Author: Andrei Popescu, TU Muenchen |
2 Author: Andrei Popescu, TU Muenchen |
3 Copyright 2012 |
3 Copyright 2012 |
4 |
4 |
5 Preliminaries. |
5 Preliminaries. |
6 *) |
6 *) |
7 |
7 |
8 header {* Preliminaries *} |
8 header {* Preliminaries *} |
9 |
9 |
10 theory Prelim |
10 theory Prelim |
11 imports "../../Codatatype/Codatatype" |
11 imports "../../BNF" |
12 begin |
12 begin |
13 |
13 |
14 declare fset_to_fset[simp] |
14 declare fset_to_fset[simp] |
15 |
15 |
16 lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s" |
16 lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s" |