src/HOL/Library/cconv.ML
6 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-04-13 noschinl 2015-04-13 rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
2015-04-13 noschinl 2015-04-13 rewrite: propagate premises to new subgoals
2015-04-13 noschinl 2015-04-13 reformat comments
2015-04-13 noschinl 2015-04-13 rewr_cconv: ignore premises when tuning conclusion
2015-04-08 wenzelm 2015-04-08 more standard Isabelle/ML tool setup; proper file headers; tuned whitespace;
2015-03-18 noschinl 2015-03-18 added proof method rewrite