equal
deleted
inserted
replaced
4 |
4 |
5 Probably this structure can be dropped due to improved reflection in Isabelle. |
5 Probably this structure can be dropped due to improved reflection in Isabelle. |
6 *) |
6 *) |
7 signature THEOREM_ISAC = |
7 signature THEOREM_ISAC = |
8 sig |
8 sig |
|
9 val numerals_to_Free: thm -> thm |
9 |
10 |
10 end |
11 end |
11 |
12 |
12 (**) |
13 (**) |
13 structure ThmC(**): THEOREM_ISAC(**) = |
14 structure ThmC(**): THEOREM_ISAC(**) = |
14 struct |
15 struct |
15 (**) |
16 (**) |
16 |
17 |
|
18 type thmID = ThmC_Def.thmID; |
|
19 type thm' = thmID * TermC.as_string; |
|
20 |
|
21 val numerals_to_Free = ThmC_Def.numerals_to_Free |
17 |
22 |
18 end |
23 end |