equal
deleted
inserted
replaced
31 * Provers/trancl.ML: new transitivity reasoner for transitive and |
31 * Provers/trancl.ML: new transitivity reasoner for transitive and |
32 reflexive-transitive closure of relations. |
32 reflexive-transitive closure of relations. |
33 |
33 |
34 * Provers/blast.ML: new reference depth_limit to make blast's depth |
34 * Provers/blast.ML: new reference depth_limit to make blast's depth |
35 limit (previously hard-coded with a value of 20) user-definable. |
35 limit (previously hard-coded with a value of 20) user-definable. |
|
36 |
|
37 * Pure: thin_tac now works even if the assumption being deleted contains !! or ==>. |
|
38 More generally, erule now works even if the major premise of the elimination rule |
|
39 contains !! or ==>. |
36 |
40 |
37 * Pure: considerably improved version of 'constdefs' command. Now |
41 * Pure: considerably improved version of 'constdefs' command. Now |
38 performs automatic type-inference of declared constants; additional |
42 performs automatic type-inference of declared constants; additional |
39 support for local structure declarations (cf. locales and HOL |
43 support for local structure declarations (cf. locales and HOL |
40 records), see also isar-ref manual. Potential INCOMPATIBILITY: need |
44 records), see also isar-ref manual. Potential INCOMPATIBILITY: need |