| Thu, 05 Oct 2006 05:46:32 +0200 | huffman | reorganize and speed up termdiffs proofs | changeset | files |
| Wed, 04 Oct 2006 18:41:14 +0200 | nipkow | fixed bug in linear arith | changeset | files |
| Wed, 04 Oct 2006 15:10:44 +0200 | haftmann | improvements for Haskell serialization | changeset | files |
| Wed, 04 Oct 2006 14:25:47 +0200 | haftmann | insert replacing ins ins_int ins_string | changeset | files |
| Wed, 04 Oct 2006 14:17:47 +0200 | haftmann | cleaned up some mess | changeset | files |
| Wed, 04 Oct 2006 14:17:46 +0200 | haftmann | clarified header comments | changeset | files |
| Wed, 04 Oct 2006 14:17:38 +0200 | haftmann | insert replacing ins ins_int ins_string | changeset | files |
| Wed, 04 Oct 2006 14:14:33 +0200 | haftmann | *** empty log message *** | changeset | files |
| Wed, 04 Oct 2006 11:50:37 +0200 | webertj | tuned | changeset | files |
| Wed, 04 Oct 2006 11:18:39 +0200 | krauss | Improved error reporting | changeset | files |
| Wed, 04 Oct 2006 01:43:57 +0200 | webertj | nnf_simpset built statically | changeset | files |
| Tue, 03 Oct 2006 19:40:34 +0200 | huffman | rewrite proofs of powser_insidea and termdiffs_aux | changeset | files |
| Mon, 02 Oct 2006 23:15:35 +0200 | huffman | generalize summability lemmas using class banach | changeset | files |
| Mon, 02 Oct 2006 23:01:14 +0200 | haftmann | clarified setup name | changeset | files |
| Mon, 02 Oct 2006 23:01:11 +0200 | haftmann | various code refinements | changeset | files |
| Mon, 02 Oct 2006 23:01:09 +0200 | haftmann | fixed some Haskell issues | changeset | files |
| Mon, 02 Oct 2006 23:01:05 +0200 | haftmann | changed preprocessing framework | changeset | files |
| Mon, 02 Oct 2006 23:01:04 +0200 | haftmann | clarified some things | changeset | files |
| Mon, 02 Oct 2006 23:01:03 +0200 | haftmann | cleaned and extended | changeset | files |
| Mon, 02 Oct 2006 23:01:00 +0200 | haftmann | added gen_primrec | changeset | files |
| Mon, 02 Oct 2006 23:00:58 +0200 | haftmann | added code for insert | changeset | files |
| Mon, 02 Oct 2006 23:00:57 +0200 | haftmann | improvements for code_gen | changeset | files |
| Mon, 02 Oct 2006 23:00:56 +0200 | haftmann | cleaned mess | changeset | files |
| Mon, 02 Oct 2006 23:00:53 +0200 | haftmann | added example for code_gen | changeset | files |
| Mon, 02 Oct 2006 23:00:52 +0200 | haftmann | dropped obsolete Theory.sign_of | changeset | files |
| Mon, 02 Oct 2006 23:00:51 +0200 | haftmann | tuned | changeset | files |
| Mon, 02 Oct 2006 23:00:50 +0200 | haftmann | added code generator names for nat_rec and nat_case | changeset | files |
| Mon, 02 Oct 2006 23:00:49 +0200 | haftmann | improved serialization for arbitrary | changeset | files |
| Mon, 02 Oct 2006 23:00:46 +0200 | haftmann | normal_form now a diagnostic command | changeset | files |
| Mon, 02 Oct 2006 23:00:45 +0200 | haftmann | restructured contents | changeset | files |
| Mon, 02 Oct 2006 21:30:05 +0200 | huffman | add axclass banach for complete normed vector spaces | changeset | files |
| Mon, 02 Oct 2006 19:57:02 +0200 | huffman | remove unused Cauchy_Bseq lemmas | changeset | files |
| Mon, 02 Oct 2006 18:30:10 +0200 | huffman | add lemmas norm_not_less_zero, norm_le_zero_iff | changeset | files |
| Mon, 02 Oct 2006 17:33:13 +0200 | paulson | added is_Trueprop | changeset | files |
| Mon, 02 Oct 2006 17:32:18 +0200 | paulson | tidying and simplifying | changeset | files |
| Mon, 02 Oct 2006 17:32:03 +0200 | paulson | Changing the default for theory_const | changeset | files |
| Mon, 02 Oct 2006 17:31:14 +0200 | paulson | extensions for Susanto | changeset | files |
| Mon, 02 Oct 2006 17:30:56 +0200 | paulson | restored the "length of name > 2" check for package definitions | changeset | files |
| Mon, 02 Oct 2006 17:29:42 +0200 | paulson | Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc. | changeset | files |
| Sun, 01 Oct 2006 22:19:24 +0200 | wenzelm | exists_name: include this theory name; | changeset | files |
| Sun, 01 Oct 2006 22:19:23 +0200 | wenzelm | removed obsolete Datatype_Universe.thy (cf. Datatype.thy); | changeset | files |
| Sun, 01 Oct 2006 22:19:21 +0200 | wenzelm | merged with theory Datatype_Universe; | changeset | files |
| Sun, 01 Oct 2006 18:30:04 +0200 | wenzelm | obsolete; | changeset | files |
| Sun, 01 Oct 2006 18:29:36 +0200 | wenzelm | renamed ex/SVC_Oracle.ML to ex/svc_oracle.ML; | changeset | files |
| Sun, 01 Oct 2006 18:29:35 +0200 | wenzelm | removed share_data; | changeset | files |
| Sun, 01 Oct 2006 18:29:34 +0200 | wenzelm | cterm_match: avoid recalculation of maxidx; | changeset | files |
| Sun, 01 Oct 2006 18:29:33 +0200 | wenzelm | reverted to revision 1.28; | changeset | files |
| Sun, 01 Oct 2006 18:29:32 +0200 | wenzelm | proper use of svc_oracle.ML; | changeset | files |
| Sun, 01 Oct 2006 18:29:31 +0200 | wenzelm | reactivated theory PER; | changeset | files |
| Sun, 01 Oct 2006 18:29:30 +0200 | wenzelm | tuned proofs; | changeset | files |
| Sun, 01 Oct 2006 18:29:28 +0200 | wenzelm | moved theory Infinite_Set to Library; | changeset | files |
| Sun, 01 Oct 2006 18:29:26 +0200 | wenzelm | moved theory Infinite_Set to Library; | changeset | files |
| Sun, 01 Oct 2006 18:29:25 +0200 | wenzelm | moved Infinite_Set.thy to Library; | changeset | files |
| Sun, 01 Oct 2006 18:29:23 +0200 | wenzelm | tuned; | changeset | files |
| Sun, 01 Oct 2006 12:07:57 +0200 | mengj | Removed the helper files (combinator rewrite rules, function extensionality and fequal rules). | changeset | files |
| Sun, 01 Oct 2006 03:07:12 +0200 | huffman | generalize more DERIV proofs | changeset | files |
| Sat, 30 Sep 2006 21:39:31 +0200 | wenzelm | statement: Variable.fix_frees; | changeset | files |
| Sat, 30 Sep 2006 21:39:29 +0200 | wenzelm | added undo_end; | changeset | files |
| Sat, 30 Sep 2006 21:39:27 +0200 | wenzelm | tuned proofs; | changeset | files |
| Sat, 30 Sep 2006 21:39:25 +0200 | wenzelm | proper import of Main HOL; | changeset | files |