equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Generic theorem transfer using relations *} |
6 header {* Generic theorem transfer using relations *} |
7 |
7 |
8 theory Transfer |
8 theory Transfer |
9 imports Hilbert_Choice BNF_FP_Base Metis Option |
9 imports Hilbert_Choice Metis Option |
10 begin |
10 begin |
11 |
11 |
12 (* We include Option here although it's not needed here. |
12 (* We include Option here although it's not needed here. |
13 By doing this, we avoid a diamond problem for BNF and |
13 By doing this, we avoid a diamond problem for BNF and |
14 FP sugar interpretation defined in this file. *) |
14 FP sugar interpretation defined in this file. *) |