2014-02-10 removed rotten code;
wenzelm [Mon, 10 Feb 2014 13:47:31 +0100] rev 55378
removed rotten code;
2014-02-10 more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example:
wenzelm [Mon, 10 Feb 2014 13:04:08 +0100] rev 55377
more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example: lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))" using [[simp_depth_limit = 1]] apply simp oops
2014-02-10 merged
nipkow [Mon, 10 Feb 2014 21:51:15 +0100] rev 55376
merged
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 tip