| Mon, 08 Aug 2011 11:25:18 -0700 | huffman | declare {INF,SUP}_empty [simp] | changeset | files |
| Mon, 08 Aug 2011 10:32:55 -0700 | huffman | rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too) | changeset | files |
| Mon, 08 Aug 2011 10:26:26 -0700 | huffman | standard theorem naming scheme: complex_eqI, complex_eq_iff | changeset | files |
| Mon, 08 Aug 2011 09:52:09 -0700 | huffman | moved division ring stuff from Rings.thy to Fields.thy | changeset | files |
| Mon, 08 Aug 2011 08:55:49 -0700 | huffman | Library/Product_ord: wellorder instance for products | changeset | files |
| Mon, 08 Aug 2011 21:11:10 +0200 | wenzelm | modernized file proof_checker.ML; | changeset | files |
| Mon, 08 Aug 2011 20:47:12 +0200 | wenzelm | tuned thm_of_proof: build lookup table within closure; | changeset | files |
| Mon, 08 Aug 2011 20:21:49 +0200 | wenzelm | added Reconstruct.proof_of convenience; | changeset | files |