equal
deleted
inserted
replaced
87 * Command '\<proof>' is an alias for 'sorry', with different |
87 * Command '\<proof>' is an alias for 'sorry', with different |
88 typesetting. E.g. to produce proof holes in examples and documentation. |
88 typesetting. E.g. to produce proof holes in examples and documentation. |
89 |
89 |
90 * The old proof method "default" has been removed (legacy since |
90 * The old proof method "default" has been removed (legacy since |
91 Isabelle2016). INCOMPATIBILITY, use "standard" instead. |
91 Isabelle2016). INCOMPATIBILITY, use "standard" instead. |
|
92 |
|
93 |
|
94 *** Pure *** |
|
95 |
|
96 * Code generator: config option "code_timinger" triggers |
|
97 measurements of different phases of code generation. See |
|
98 src/HOL/ex/Code_Timing.thy for examples. |
92 |
99 |
93 |
100 |
94 *** HOL *** |
101 *** HOL *** |
95 |
102 |
96 * Probability/Random_Permutations.thy contains some theory about |
103 * Probability/Random_Permutations.thy contains some theory about |