src/HOL/Library/rewrite.ML
2016-06-11 wenzelm 2016-06-11 clarified syntax;
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
2015-10-18 wenzelm 2015-10-18 tuned signature;
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-17 wenzelm 2015-04-17 make SML/NJ happy;
2015-04-17 noschinl 2015-04-17 rewrite: work purely conversion-based
2015-04-17 noschinl 2015-04-17 merged
2015-04-17 noschinl 2015-04-17 rewrite: add default pattern "in concl" for more cases
2015-04-16 wenzelm 2015-04-16 make SML/NJ happy;
2015-04-16 noschinl 2015-04-16 rewrite: use distinct names for unnamed abstractions
2015-04-15 noschinl 2015-04-15 rewrite: add ML interface
2015-04-14 noschinl 2015-04-14 rewrite: tuned code, no semantic changes
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: do not descend into conclusion of premise with asm pattern
2015-04-13 noschinl 2015-04-13 rewrite: with asm pattern, try all premises for rewriting, not only the first
2015-04-13 noschinl 2015-04-13 tuned
2015-04-13 noschinl 2015-04-13 rewrite: propagate premises to new subgoals
2015-04-08 wenzelm 2015-04-08 more standard Isabelle/ML tool setup; proper file headers; tuned whitespace;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-03-18 noschinl 2015-03-18 added proof method rewrite