equal
deleted
inserted
replaced
64 that only know about meta-equality (==). Potential INCOMPATIBILITY in |
64 that only know about meta-equality (==). Potential INCOMPATIBILITY in |
65 theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order |
65 theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order |
66 is relevant to avoid confusion of Pure.simp vs. HOL.simp. |
66 is relevant to avoid confusion of Pure.simp vs. HOL.simp. |
67 |
67 |
68 * Commands 'prf' and 'full_prf' are somewhat more informative (again): |
68 * Commands 'prf' and 'full_prf' are somewhat more informative (again): |
69 proof terms are reconstructed and cleaned from administrative thm nodes. |
69 proof terms are reconstructed and cleaned from administrative thm |
|
70 nodes. |
|
71 |
|
72 * The command 'unfolding' and proof method "unfold" include a second |
|
73 stage where given equations are passed through the attribute "abs_def" |
|
74 before rewriting. This ensures that definitions are fully expanded, |
|
75 regardless of the actual parameters that are provided. Rare |
|
76 INCOMPATIBILITY in some corner cases: use proof method (simp only:) |
|
77 instead, or declare [[unfold_abs_def = false]] in the proof context. |
70 |
78 |
71 |
79 |
72 *** Prover IDE -- Isabelle/Scala/jEdit *** |
80 *** Prover IDE -- Isabelle/Scala/jEdit *** |
73 |
81 |
74 * Cartouche abbreviations work both for " and ` to accomodate typical |
82 * Cartouche abbreviations work both for " and ` to accomodate typical |