| Tue, 07 Nov 2006 11:28:25 +0100 | berghofe | Adapted to changes in FixedPoint theory. | changeset | files |
| Tue, 07 Nov 2006 09:59:43 +0100 | krauss | method exported | changeset | files |
| Tue, 07 Nov 2006 09:41:14 +0100 | krauss | updated NEWS | changeset | files |
| Tue, 07 Nov 2006 09:33:47 +0100 | krauss | * Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. | changeset | files |
| Tue, 07 Nov 2006 08:03:46 +0100 | haftmann | added gfx | changeset | files |
| Mon, 06 Nov 2006 16:29:21 +0100 | haftmann | dropped blastdata.ML | changeset | files |
| Mon, 06 Nov 2006 16:28:37 +0100 | haftmann | (adjustions) | changeset | files |
| Mon, 06 Nov 2006 16:28:36 +0100 | haftmann | two further lemmas on split | changeset | files |
| Mon, 06 Nov 2006 16:28:35 +0100 | haftmann | removed dependency of ord on eq | changeset | files |
| Mon, 06 Nov 2006 16:28:34 +0100 | haftmann | removed itrev as inlining theorem | changeset | files |
| Mon, 06 Nov 2006 16:28:33 +0100 | haftmann | added state monad to HOL library | changeset | files |
| Mon, 06 Nov 2006 16:28:31 +0100 | haftmann | code generator module naming improved | changeset | files |
| Mon, 06 Nov 2006 16:28:30 +0100 | haftmann | (continued) | changeset | files |
| Mon, 06 Nov 2006 16:28:29 +0100 | haftmann | (continued) | changeset | files |
| Mon, 06 Nov 2006 12:04:44 +0100 | krauss | minor cleanup | changeset | files |
| Sun, 05 Nov 2006 21:44:42 +0100 | wenzelm | case_tr: do not intern already internal consts; | changeset | files |
| Sun, 05 Nov 2006 21:44:41 +0100 | wenzelm | updated; | changeset | files |
| Sun, 05 Nov 2006 21:44:40 +0100 | wenzelm | removed isactrlconst; | changeset | files |
| Sun, 05 Nov 2006 21:44:39 +0100 | wenzelm | instantiate: avoid global references; | changeset | files |
| Sun, 05 Nov 2006 21:44:37 +0100 | wenzelm | added const_syntax_name; | changeset | files |
| Sun, 05 Nov 2006 21:44:35 +0100 | wenzelm | removed obsolete first_duplicate; | changeset | files |
| Sun, 05 Nov 2006 21:44:34 +0100 | wenzelm | added syntax_name; | changeset | files |
| Sun, 05 Nov 2006 21:44:33 +0100 | wenzelm | fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names; | changeset | files |
| Sun, 05 Nov 2006 21:44:32 +0100 | wenzelm | Sign.const_syntax_name; | changeset | files |
| Sun, 05 Nov 2006 09:36:25 +0100 | haftmann | added gfx | changeset | files |
| Sat, 04 Nov 2006 19:25:43 +0100 | wenzelm | removed checkpoint interface; | changeset | files |
| Sat, 04 Nov 2006 19:25:43 +0100 | wenzelm | String.compare: slow version -- performance test; | changeset | files |
| Sat, 04 Nov 2006 19:25:41 +0100 | wenzelm | replaced apply_copy by apply'; | changeset | files |
| Sat, 04 Nov 2006 19:25:41 +0100 | wenzelm | removed is_Trueprop (use can dest_Trueprop'' instead); | changeset | files |
| Sat, 04 Nov 2006 19:25:40 +0100 | wenzelm | removed is_Trueprop (use can dest_Trueprop'' instead); | changeset | files |
| Sat, 04 Nov 2006 19:25:39 +0100 | wenzelm | updated; | changeset | files |
| Sat, 04 Nov 2006 19:25:38 +0100 | wenzelm | HOL_USEDIR_OPTIONS: -p 1 by default; | changeset | files |
| Sat, 04 Nov 2006 19:25:36 +0100 | wenzelm | tuned; | changeset | files |
| Sat, 04 Nov 2006 19:25:34 +0100 | wenzelm | * October 2006: Stefan Hohe, TUM; | changeset | files |
| Sat, 04 Nov 2006 13:19:04 +0100 | wenzelm | replaced Toplevel.proof_to_theory by Toplevel.end_proof; | changeset | files |
| Sat, 04 Nov 2006 12:53:35 +0100 | wenzelm | optional argument for timespan (default 100); | changeset | files |
| Sat, 04 Nov 2006 12:46:40 +0100 | wenzelm | added at-mac-poly-e, at64-poly-e; | changeset | files |
| Sat, 04 Nov 2006 00:12:06 +0100 | huffman | moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs | changeset | files |
| Sat, 04 Nov 2006 00:11:11 +0100 | huffman | new Deriv.thy contains stuff from Lim.thy | changeset | files |
| Fri, 03 Nov 2006 15:28:13 +0100 | haftmann | re-added simpdata.ML | changeset | files |
| Fri, 03 Nov 2006 14:22:48 +0100 | haftmann | new ML serializer | changeset | files |
| Fri, 03 Nov 2006 14:22:47 +0100 | haftmann | fixed problem with eta-expansion | changeset | files |
| Fri, 03 Nov 2006 14:22:46 +0100 | haftmann | tuned | changeset | files |
| Fri, 03 Nov 2006 14:22:45 +0100 | haftmann | fixed problem with variable names | changeset | files |
| Fri, 03 Nov 2006 14:22:44 +0100 | haftmann | tightened notion of function equations | changeset | files |
| Fri, 03 Nov 2006 14:22:43 +0100 | haftmann | dropped name_mangler.ML | changeset | files |
| Fri, 03 Nov 2006 14:22:42 +0100 | haftmann | some example tweaking | changeset | files |
| Fri, 03 Nov 2006 14:22:41 +0100 | haftmann | added particular test for partially applied case constants | changeset | files |
| Fri, 03 Nov 2006 14:22:40 +0100 | haftmann | improved evaluation setup | changeset | files |
| Fri, 03 Nov 2006 14:22:39 +0100 | haftmann | adapted to changes in codegen_data.ML | changeset | files |
| Fri, 03 Nov 2006 14:22:38 +0100 | haftmann | added code gen II | changeset | files |
| Fri, 03 Nov 2006 14:22:37 +0100 | haftmann | simplified reasoning tools setup | changeset | files |
| Fri, 03 Nov 2006 14:22:36 +0100 | haftmann | dropped prop_cs | changeset | files |
| Fri, 03 Nov 2006 14:22:35 +0100 | haftmann | dropped equals_conv for nbe | changeset | files |
| Fri, 03 Nov 2006 14:22:34 +0100 | haftmann | first version of style guide | changeset | files |
| Fri, 03 Nov 2006 14:22:33 +0100 | haftmann | continued tutorial | changeset | files |
| Fri, 03 Nov 2006 14:22:31 +0100 | haftmann | added serialization keywords | changeset | files |
| Thu, 02 Nov 2006 14:27:18 +0100 | dixon | bugfix to zipto: left and right were wrong way around. | changeset | files |
| Thu, 02 Nov 2006 13:35:09 +0100 | nipkow | added sum_squared | changeset | files |
| Wed, 01 Nov 2006 19:07:37 +0100 | urbanc | changed a misplaced "also" to a "moreover" (caused a loop somehow) | changeset | files |