equal
deleted
inserted
replaced
6 |
6 |
7 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
7 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
8 |
8 |
9 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement |
9 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement |
10 |
10 |
11 *** Proof tools *** |
11 * ZF: The con_defs part of an inductive definition may no longer refer to |
12 |
12 constants declared in the same theory; |
13 * Provers/Arith/fast_lin_arith.ML contains a functor for creating a decision |
13 |
14 procedure for linear arithmetic. Currently it is used for types `nat' and |
|
15 `int' in HOL (see below) but can, should and will be instantiated for other |
|
16 types and logics as well. |
|
17 |
14 |
18 *** General *** |
15 *** General *** |
19 |
16 |
20 * in locales, the "assumes" and "defines" parts may be omitted if empty; |
17 * in locales, the "assumes" and "defines" parts may be omitted if empty; |
21 |
18 |
51 include \n in its semantics, forcing writeln to add one |
48 include \n in its semantics, forcing writeln to add one |
52 uncoditionally; replaced prs_fn by writeln_fn; consider std_output: |
49 uncoditionally; replaced prs_fn by writeln_fn; consider std_output: |
53 string -> unit if you really want to output text without newline; |
50 string -> unit if you really want to output text without newline; |
54 |
51 |
55 |
52 |
|
53 *** ZF *** |
|
54 |
|
55 * new primrec section allows primitive recursive functions to be given |
|
56 directly, as in HOL; |
|
57 |
|
58 * new tactics induct_tac and exhaust_tac for induction (or case analysis) |
|
59 on a datatype; |
|
60 |
|
61 * the datatype declaration of type T now defines the recursor T_rec; |
|
62 |
|
63 |
56 New in Isabelle98-1 (October 1998) |
64 New in Isabelle98-1 (October 1998) |
57 ---------------------------------- |
65 ---------------------------------- |
58 |
66 |
59 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
67 *** Overview of INCOMPATIBILITIES (see below for more details) *** |
60 |
68 |