equal
deleted
inserted
replaced
14 theory LocaleTest2 |
14 theory LocaleTest2 |
15 imports Main |
15 imports Main |
16 begin |
16 begin |
17 |
17 |
18 ML {* set quick_and_dirty *} (* allow for thm command in batch mode *) |
18 ML {* set quick_and_dirty *} (* allow for thm command in batch mode *) |
19 ML {* set Toplevel.debug *} |
|
20 ML {* set show_hyps *} |
19 ML {* set show_hyps *} |
21 ML {* set show_sorts *} |
20 ML {* set show_sorts *} |
22 |
21 |
23 section {* Interpretation of Defined Concepts *} |
22 section {* Interpretation of Defined Concepts *} |
24 |
23 |