equal
deleted
inserted
replaced
70 > (defconst proofstate-proofstart-regexp "^Level [0-9]+" |
70 > (defconst proofstate-proofstart-regexp "^Level [0-9]+" |
71 |
71 |
72 |
72 |
73 *** HOL *** |
73 *** HOL *** |
74 |
74 |
75 * recdef (TFL) now requires theory Recdef; |
|
76 |
|
77 * There are now decision procedures for linear arithmetic over nat and |
75 * There are now decision procedures for linear arithmetic over nat and |
78 int: |
76 int: |
79 |
77 |
80 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', |
78 1. arith_tac copes with arbitrary formulae involving `=', `<', `<=', |
81 `+', `-', `Suc', `min', `max' and numerical constants; other subterms |
79 `+', `-', `Suc', `min', `max' and numerical constants; other subterms |
104 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
102 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
105 changed syntax and (many) tactics; |
103 changed syntax and (many) tactics; |
106 |
104 |
107 * HOL/typedef: fixed type inference for representing set; type |
105 * HOL/typedef: fixed type inference for representing set; type |
108 arguments now have to occur explicitly on the rhs as type constraints; |
106 arguments now have to occur explicitly on the rhs as type constraints; |
|
107 |
|
108 * HOL/recdef (TFL) now requires theory Recdef; |
109 |
109 |
110 |
110 |
111 *** ZF *** |
111 *** ZF *** |
112 |
112 |
113 * new primrec section allows primitive recursive functions to be given |
113 * new primrec section allows primitive recursive functions to be given |