equal
deleted
inserted
replaced
15 '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed |
15 '\<Pi>x. ...', which is now a type error since \<Pi>x will be parsed |
16 as an identifier. Fix it by inserting a space around former |
16 as an identifier. Fix it by inserting a space around former |
17 symbols. Call 'isatool fixgreek' to try to fix parsing errors in |
17 symbols. Call 'isatool fixgreek' to try to fix parsing errors in |
18 existing theory and ML files. |
18 existing theory and ML files. |
19 |
19 |
|
20 * Pure: Using the functions Theory.add_finals or Theory.add_finals_i |
|
21 or the new Isar command "finalconsts", it is now possible to |
|
22 make constants "final", thereby ensuring that they are not defined |
|
23 later. Useful for constants whose behaviour is fixed axiomatically |
|
24 rather than definitionally, such as the meta-logic connectives. |
|
25 |
20 *** Isar *** |
26 *** Isar *** |
21 |
27 |
22 * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac: |
28 * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac: |
23 - Now understand static (Isar) contexts. As a consequence, users of Isar |
29 - Now understand static (Isar) contexts. As a consequence, users of Isar |
24 locales are no longer forced to write Isar proof scripts. |
30 locales are no longer forced to write Isar proof scripts. |
40 (Isar) contexts. |
46 (Isar) contexts. |
41 |
47 |
42 *** HOL *** |
48 *** HOL *** |
43 |
49 |
44 * 'specification' command added, allowing for definition by |
50 * 'specification' command added, allowing for definition by |
45 specification. |
51 specification. There is also an 'ax_specification' command that |
|
52 introduces the new constants axiomatically. |
46 |
53 |
47 * SET-Protocol: formalization and verification of the SET protocol suite; |
54 * SET-Protocol: formalization and verification of the SET protocol suite; |
48 |
55 |
49 |
56 |
50 New in Isabelle2003 (May 2003) |
57 New in Isabelle2003 (May 2003) |