equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 section \<open>Benchmark Consisting of Datatypes Defined in IsaFoR\<close> |
8 section \<open>Benchmark Consisting of Datatypes Defined in IsaFoR\<close> |
9 |
9 |
10 theory IsaFoR |
10 theory IsaFoR |
11 imports Real |
11 imports HOL.Real |
12 begin |
12 begin |
13 |
13 |
14 datatype (discs_sels) ('f, 'l) lab = |
14 datatype (discs_sels) ('f, 'l) lab = |
15 Lab "('f, 'l) lab" 'l |
15 Lab "('f, 'l) lab" 'l |
16 | FunLab "('f, 'l) lab" "('f, 'l) lab list" |
16 | FunLab "('f, 'l) lab" "('f, 'l) lab list" |