| Mon, 18 Feb 2013 18:34:54 +0100 | blanchet | tuning | changeset | files |
| Mon, 18 Feb 2013 12:16:27 +0100 | smolkas | split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations | changeset | files |
| Mon, 18 Feb 2013 12:16:02 +0100 | smolkas | simplified byline, isar_qualifier | changeset | files |
| Mon, 18 Feb 2013 11:33:43 +0100 | blanchet | tuned code: factored out parent computation | changeset | files |
| Mon, 18 Feb 2013 10:43:36 +0100 | blanchet | tuned code | changeset | files |
| Mon, 18 Feb 2013 08:52:23 +0100 | Andreas Lochbihler | simplify definition as sort constraints ensure finiteness (thanks to Jesus Aransay) | changeset | files |