Fri, 27 Jul 2012 20:05:56 +0200 restored narrowing quickcheck after 6efff142bb54
haftmann [Fri, 27 Jul 2012 20:05:56 +0200] rev 48565
restored narrowing quickcheck after 6efff142bb54
Fri, 27 Jul 2012 21:50:34 +0200 tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
wenzelm [Fri, 27 Jul 2012 21:50:34 +0200] rev 48564
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
Fri, 27 Jul 2012 20:58:44 +0200 unvarify thm statement stemming from old-style definition, to avoid schematic type variables in subsequent goal;
wenzelm [Fri, 27 Jul 2012 20:58:44 +0200] rev 48563
unvarify thm statement stemming from old-style definition, to avoid schematic type variables in subsequent goal;
Fri, 27 Jul 2012 19:57:23 +0200 tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
wenzelm [Fri, 27 Jul 2012 19:57:23 +0200] rev 48562
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
Fri, 27 Jul 2012 19:27:21 +0200 move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
huffman [Fri, 27 Jul 2012 19:27:21 +0200] rev 48561
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
Fri, 27 Jul 2012 17:59:18 +0200 replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
huffman [Fri, 27 Jul 2012 17:59:18 +0200] rev 48560
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
Fri, 27 Jul 2012 17:57:31 +0200 give Nat_Arith simprocs proper name bindings by using simproc_setup
huffman [Fri, 27 Jul 2012 17:57:31 +0200] rev 48559
give Nat_Arith simprocs proper name bindings by using simproc_setup
Fri, 27 Jul 2012 17:34:33 +0200 tweaks in preparation for type encoding evaluation
blanchet [Fri, 27 Jul 2012 17:34:33 +0200] rev 48558
tweaks in preparation for type encoding evaluation
Fri, 27 Jul 2012 16:35:02 +0200 merged
wenzelm [Fri, 27 Jul 2012 16:35:02 +0200] rev 48557
merged
Fri, 27 Jul 2012 15:42:39 +0200 replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman [Fri, 27 Jul 2012 15:42:39 +0200] rev 48556
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip