equal
deleted
inserted
replaced
12 |
12 |
13 New in Isabelle99-2 (February 2001) |
13 New in Isabelle99-2 (February 2001) |
14 ----------------------------------- |
14 ----------------------------------- |
15 |
15 |
16 *** Overview of INCOMPATIBILITIES *** |
16 *** Overview of INCOMPATIBILITIES *** |
|
17 |
|
18 * HOL: please note that theories in the Library and elsewhere often use the |
|
19 new-style (Isar) format; to refer to their theorems in an ML script you must |
|
20 bind them to ML identifers by e.g. val thm_name = thm "thm_name"; |
17 |
21 |
18 * HOL: inductive package no longer splits induction rule aggressively, |
22 * HOL: inductive package no longer splits induction rule aggressively, |
19 but only as far as specified by the introductions given; the old |
23 but only as far as specified by the introductions given; the old |
20 format may be recovered via ML function complete_split_rule or attribute |
24 format may be recovered via ML function complete_split_rule or attribute |
21 'split_rule (complete)'; |
25 'split_rule (complete)'; |