src/HOL/ex/Rewrite_Examples.thy
2015-04-17 noschinl 2015-04-17 rewrite: work purely conversion-based
2015-04-17 noschinl 2015-04-17 rewrite: add default pattern "in concl" for more cases
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-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 rewrite: propagate premises to new subgoals
2015-04-13 noschinl 2015-04-13 enable \<hole> syntax for rewrite
2015-03-18 noschinl 2015-03-18 added proof method rewrite