equal
deleted
inserted
replaced
20 ``var x + var y + struct M'' as import; |
20 ``var x + var y + struct M'' as import; |
21 |
21 |
22 * Pure: improved thms_containing: proper indexing of facts instead of |
22 * Pure: improved thms_containing: proper indexing of facts instead of |
23 raw theorems; check validity of results wrt. current name space; |
23 raw theorems; check validity of results wrt. current name space; |
24 include local facts of proof configuration (also covers active |
24 include local facts of proof configuration (also covers active |
25 locales); an optional limit for the number of printed facts may be |
25 locales), cover fixed variables in index; may use "_" in term |
26 given (the default is 40); |
26 specification; an optional limit for the number of printed facts may |
27 |
27 be given (the default is 40); |
28 * Pure: disallow duplicate fact bindings within new-style theory |
28 |
29 files; |
29 * Pure: disallow duplicate fact bindings within new-style theory files |
|
30 (batch-mode only); |
30 |
31 |
31 * Provers: improved induct method: assumptions introduced by case |
32 * Provers: improved induct method: assumptions introduced by case |
32 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from |
33 "foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from |
33 the goal statement); "foo" still refers to all facts collectively; |
34 the goal statement); "foo" still refers to all facts collectively; |
34 |
35 |