Wed, 13 Jul 2016 19:10:35 +0200 | wenzelm | clarified indentation of proof commands, notably for "notepad begin", which lacks a head goal; | changeset | files |
Wed, 13 Jul 2016 19:04:49 +0200 | wenzelm | clarified indentation: 'begin' is treated like a separate command without indent; | changeset | files |