| Mon, 14 May 2007 09:11:30 +0200 | huffman | remove redundant lemmas | changeset | files |
| Mon, 14 May 2007 08:15:13 +0200 | huffman | cleaned up | changeset | files |
| Mon, 14 May 2007 08:12:38 +0200 | huffman | tuned | changeset | files |
| Sun, 13 May 2007 20:05:42 +0200 | huffman | define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously | changeset | files |
| Sun, 13 May 2007 19:15:36 +0200 | huffman | add lemma power_eq_imp_eq_base | changeset | files |
| Sun, 13 May 2007 18:16:49 +0200 | haftmann | added module int | changeset | files |
| Sun, 13 May 2007 18:15:30 +0200 | haftmann | dropped legacy | changeset | files |
| Sun, 13 May 2007 18:15:28 +0200 | haftmann | removed module rat.ML | changeset | files |
| Sun, 13 May 2007 18:15:26 +0200 | haftmann | whitespace tuned | changeset | files |
| Sun, 13 May 2007 18:15:25 +0200 | haftmann | tuned | changeset | files |
| Sun, 13 May 2007 18:15:24 +0200 | haftmann | fixed omission | changeset | files |
| Sun, 13 May 2007 18:15:23 +0200 | haftmann | tuned setup | changeset | files |
| Sun, 13 May 2007 18:15:22 +0200 | haftmann | refined module rat | changeset | files |
| Sun, 13 May 2007 18:15:21 +0200 | haftmann | added modules rat.ML and int.ML | changeset | files |
| Sun, 13 May 2007 09:23:27 +0200 | nipkow | Removed junk | changeset | files |
| Sun, 13 May 2007 07:11:21 +0200 | nipkow | Got rid of listsp | changeset | files |
| Sun, 13 May 2007 04:38:24 +0200 | huffman | removed redundant lemmas | changeset | files |
| Sat, 12 May 2007 18:16:30 +0200 | huffman | add lemma additive.setsum | changeset | files |
| Fri, 11 May 2007 20:47:30 +0200 | nipkow | *** empty log message *** | changeset | files |
| Fri, 11 May 2007 20:07:00 +0200 | nipkow | *** empty log message *** | changeset | files |
| Fri, 11 May 2007 18:49:15 +0200 | wenzelm | proper type for fun/arg_cong_rule; | changeset | files |
| Fri, 11 May 2007 18:47:08 +0200 | wenzelm | added fun/arg_cong_rule; | changeset | files |
| Fri, 11 May 2007 18:46:50 +0200 | wenzelm | unified names: foo_conv; | changeset | files |
| Fri, 11 May 2007 17:54:36 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 11 May 2007 15:37:42 +0200 | krauss | added fun flip f x y = f y x | changeset | files |
| Fri, 11 May 2007 03:31:12 +0200 | huffman | generalize setsum lemmas from semiring_0_cancel to semiring_0 | changeset | files |
| Fri, 11 May 2007 01:07:10 +0200 | wenzelm | tuned proofs; | changeset | files |
| Fri, 11 May 2007 00:43:46 +0200 | wenzelm | bang_facts: warning; | changeset | files |
| Fri, 11 May 2007 00:43:45 +0200 | wenzelm | tuned proofs; | changeset | files |
| Thu, 10 May 2007 22:11:38 +0200 | haftmann | (class target) | changeset | files |
| Thu, 10 May 2007 22:11:37 +0200 | haftmann | cleaned up | changeset | files |
| Thu, 10 May 2007 22:11:36 +0200 | haftmann | beta/eta conversion after preprocessor | changeset | files |
| Thu, 10 May 2007 22:11:35 +0200 | haftmann | fixed typo | changeset | files |
| Thu, 10 May 2007 18:10:32 +0200 | wenzelm | more conversions; | changeset | files |
| Thu, 10 May 2007 15:51:59 +0200 | berghofe | Moved extraction_expand declaration of listall_def outside of definition. | changeset | files |
| Thu, 10 May 2007 15:50:56 +0200 | berghofe | Adapted to new naming scheme for definitions. | changeset | files |
| Thu, 10 May 2007 15:50:28 +0200 | berghofe | Changed name of raw definition. | changeset | files |
| Thu, 10 May 2007 15:49:31 +0200 | berghofe | Name of ML function "not" is now qualified in order to avoid | changeset | files |
| Thu, 10 May 2007 10:22:17 +0200 | haftmann | consts in consts_code Isar commands are now referred to by usual term syntax | changeset | files |
| Thu, 10 May 2007 10:21:50 +0200 | haftmann | size [nat] is identity | changeset | files |
| Thu, 10 May 2007 10:21:48 +0200 | haftmann | explicit import of Datatype.thy due to hook bootstrap problem | changeset | files |
| Thu, 10 May 2007 10:21:47 +0200 | haftmann | localized Sup/Inf | changeset | files |
| Thu, 10 May 2007 10:21:46 +0200 | haftmann | localized Min/Max | changeset | files |
| Thu, 10 May 2007 10:21:44 +0200 | haftmann | tuned | changeset | files |
| Thu, 10 May 2007 04:06:56 +0200 | huffman | fix proofs | changeset | files |
| Thu, 10 May 2007 03:11:03 +0200 | huffman | remove redundant lemmas | changeset | files |
| Thu, 10 May 2007 03:07:26 +0200 | huffman | lemmas iszero_(h)complex_number_of are no longer needed | changeset | files |
| Thu, 10 May 2007 03:00:15 +0200 | huffman | instance real_algebra_1 < ring_char_0 | changeset | files |
| Thu, 10 May 2007 02:51:53 +0200 | huffman | new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas | changeset | files |
| Thu, 10 May 2007 00:39:56 +0200 | wenzelm | moved conversions to structure Conv; | changeset | files |
| Thu, 10 May 2007 00:39:55 +0200 | wenzelm | added dest_fun/fun2/arg1; | changeset | files |
| Thu, 10 May 2007 00:39:54 +0200 | wenzelm | tuned argument_type_of; | changeset | files |
| Thu, 10 May 2007 00:39:53 +0200 | wenzelm | added destructors from drule.ML; | changeset | files |
| Thu, 10 May 2007 00:39:52 +0200 | wenzelm | moved some operations to more_thm.ML and conv.ML; | changeset | files |
| Thu, 10 May 2007 00:39:51 +0200 | wenzelm | Conversions: primitive equality reasoning (from drule.ML); | changeset | files |
| Thu, 10 May 2007 00:39:50 +0200 | wenzelm | added conv.ML; | changeset | files |
| Thu, 10 May 2007 00:39:49 +0200 | wenzelm | Thm.match; | changeset | files |
| Thu, 10 May 2007 00:39:48 +0200 | wenzelm | moved some Drule operations to Thm (see more_thm.ML); | changeset | files |
| Thu, 10 May 2007 00:39:46 +0200 | wenzelm | Thm.first_order_match; | changeset | files |
| Thu, 10 May 2007 00:39:45 +0200 | wenzelm | moved conversions to structure Conv; | changeset | files |