| changeset 63624 | 994d1a1105ef |
| parent 63610 | 4b40b8196dc7 |
| child 63627 | 6ddb43c6b711 |
--- a/NEWS Sat Aug 06 17:39:21 2016 +0200 +++ b/NEWS Sat Aug 06 18:14:59 2016 +0200 @@ -57,6 +57,9 @@ theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order is relevant to avoid confusion of Pure.simp vs. HOL.simp. +* Commands 'prf' and 'full_prf' are somewhat more informative (again): +proof terms are reconstructed and cleaned from administrative thm nodes. + *** Prover IDE -- Isabelle/Scala/jEdit ***