equal
deleted
inserted
replaced
125 the current simpset. |
125 the current simpset. |
126 *} |
126 *} |
127 |
127 |
128 section {* Contexts (TBD) *} |
128 section {* Contexts (TBD) *} |
129 |
129 |
|
130 ML_command "ProofContext.debug := true" |
|
131 ML_command "ProofContext.verbose := true" |
|
132 |
|
133 |
130 section {* Local Theories (TBD) *} |
134 section {* Local Theories (TBD) *} |
131 |
135 |
132 text {* |
136 text {* |
133 In contrast to an ordinary theory, which simply consists of a type |
137 In contrast to an ordinary theory, which simply consists of a type |
134 signature, as well as tables for constants, axioms and theorems, a local |
138 signature, as well as tables for constants, axioms and theorems, a local |