equal
deleted
inserted
replaced
58 |
58 |
59 * Type constructors admit general mixfix syntax, not just infix. |
59 * Type constructors admit general mixfix syntax, not just infix. |
60 |
60 |
61 * Use of cumulative prems via "!" in some proof methods has been |
61 * Use of cumulative prems via "!" in some proof methods has been |
62 discontinued (legacy feature). |
62 discontinued (legacy feature). |
|
63 |
|
64 * References 'trace_simp' and 'debug_simp' have been replaced by |
|
65 configuration options stored in the context. Enabling tracing |
|
66 (the case of debugging is similar) in proofs works via |
|
67 |
|
68 using [[trace_simp=true]] |
|
69 |
|
70 Tracing is then active for all invocations of the simplifier |
|
71 in subsequent goal refinement steps. |
63 |
72 |
64 |
73 |
65 *** Pure *** |
74 *** Pure *** |
66 |
75 |
67 * Local theory specifications may depend on extra type variables that |
76 * Local theory specifications may depend on extra type variables that |