| Thu, 09 Jul 2015 23:46:21 +0200 | wenzelm | tuned proofs; | changeset | files |
| Thu, 09 Jul 2015 22:36:31 +0200 | wenzelm | SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier); | changeset | files |
| Thu, 09 Jul 2015 22:13:24 +0200 | wenzelm | clarified specific use of inspect_contract: "any Bound variable will do" may render the term invalid for Term.fastype_of1 in inst_subst_tac (see also 7c3757fccf0e); | changeset | files |