equal
deleted
inserted
replaced
56 `nat'. It is fast and is used automatically by the simplifier. |
56 `nat'. It is fast and is used automatically by the simplifier. |
57 |
57 |
58 NB: At the moment, these decision procedures do not cope with mixed nat/int |
58 NB: At the moment, these decision procedures do not cope with mixed nat/int |
59 formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'. |
59 formulae where the two parts interact, such as `m < n ==> int(m) < int(n)'. |
60 |
60 |
|
61 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization |
|
62 -- avoids syntactic ambiguities and treats state, transition, and |
|
63 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
|
64 changed syntax and (many) tactics; |
|
65 |
61 |
66 |
62 *** Internal programming interfaces *** |
67 *** Internal programming interfaces *** |
63 |
68 |
64 * tuned current_goals_markers semantics: begin / end goal avoids |
69 * tuned current_goals_markers semantics: begin / end goal avoids |
65 printing empty lines; |
70 printing empty lines; |
67 * removed prs and prs_fn hook, which was broken because it did not |
72 * removed prs and prs_fn hook, which was broken because it did not |
68 include \n in its semantics, forcing writeln to add one |
73 include \n in its semantics, forcing writeln to add one |
69 uncoditionally; replaced prs_fn by writeln_fn; consider std_output: |
74 uncoditionally; replaced prs_fn by writeln_fn; consider std_output: |
70 string -> unit if you really want to output text without newline; |
75 string -> unit if you really want to output text without newline; |
71 |
76 |
72 * HOL/TLA (Lamport's Temporal Logic of Actions): major reorganization |
77 * Symbol.output subject to print mode; INCOMPATIBILITY: defaults to |
73 -- avoids syntactic ambiguities and treats state, transition, and |
78 plain output, interface builders may have to enable 'isabelle_font' |
74 temporal levels more uniformly; introduces INCOMPATIBILITIES due to |
79 mode to get Isabelle font glyphs as before; |
75 changed syntax and (many) tactics; |
|
76 |
80 |
77 |
81 |
78 *** ZF *** |
82 *** ZF *** |
79 |
83 |
80 * new primrec section allows primitive recursive functions to be given |
84 * new primrec section allows primitive recursive functions to be given |