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
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip