equal
deleted
inserted
replaced
14 "foo_bar". |
14 "foo_bar". |
15 |
15 |
16 |
16 |
17 *** Pure *** |
17 *** Pure *** |
18 |
18 |
19 * Instantiation target allows for simultaneous specification of class instance |
19 * Instantiation target allows for simultaneous specification of class |
20 operations together with an instantiation proof. Type check phase allows to |
20 instance operations together with an instantiation proof. |
21 refer to class operations uniformly. See HOL/Complex/Complex.thy for an Isar |
21 Type-checking phase allows to refer to class operations uniformly. |
22 example and HOL/Library/Eval.thy for an ML example. |
22 See HOL/Complex/Complex.thy for an Isar example and |
23 Superseedes some immature attempts. |
23 HOL/Library/Eval.thy for an ML example. Supersedes previous |
|
24 experimental versions. |
24 |
25 |
25 |
26 |
26 *** HOL *** |
27 *** HOL *** |
27 |
28 |
28 * Theorems "power.simps" renamed to "power_int.simps". |
29 * Theorems "power.simps" renamed to "power_int.simps". |
82 management only; user-code should use print_mode_value, |
83 management only; user-code should use print_mode_value, |
83 print_mode_active, PrintMode.setmp etc. INCOMPATIBILITY. |
84 print_mode_active, PrintMode.setmp etc. INCOMPATIBILITY. |
84 |
85 |
85 |
86 |
86 *** System *** |
87 *** System *** |
|
88 |
|
89 * Default settings: PROOFGENERAL_OPTIONS no longer impose xemacs here |
|
90 --- in accordance with Proof General 3.7, which prefers GNU emacs. |
87 |
91 |
88 * Multithreading.max_threads := 0 refers to the number of actual CPU |
92 * Multithreading.max_threads := 0 refers to the number of actual CPU |
89 cores of the underlying machine, which is a good starting point for |
93 cores of the underlying machine, which is a good starting point for |
90 optimal performance tuning. The corresponding usedir option -M allows |
94 optimal performance tuning. The corresponding usedir option -M allows |
91 "max" as an alias for "0". WARNING: does not work on certain versions |
95 "max" as an alias for "0". WARNING: does not work on certain versions |