| 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 |
| Wed, 01 Nov 2006 19:03:30 +0100 | urbanc | changed to not compile Iteration and Recursion, but Lam_Funs instead | changeset | files |
| Wed, 01 Nov 2006 17:57:02 +0100 | huffman | move DERIV_sumr from Series.thy to Lim.thy | changeset | files |
| Wed, 01 Nov 2006 17:14:16 +0100 | huffman | generalize type of lemma isCont_Id | changeset | files |
| Wed, 01 Nov 2006 16:48:58 +0100 | huffman | new proof of Bseq_NSbseq using transfer | changeset | files |
| Wed, 01 Nov 2006 16:11:31 +0100 | urbanc | changed to use Lam_Funs | changeset | files |
| Wed, 01 Nov 2006 15:51:11 +0100 | paulson | clauses for iff-introduction, unfortunately useless | changeset | files |
| Wed, 01 Nov 2006 15:50:19 +0100 | urbanc | tuned | changeset | files |
| Wed, 01 Nov 2006 15:49:43 +0100 | paulson | Numerous cosmetic changes. | changeset | files |
| Wed, 01 Nov 2006 15:45:44 +0100 | urbanc | not needed anymore | changeset | files |
| Wed, 01 Nov 2006 15:44:31 +0100 | urbanc | these files are superseded by the internal recursion combinator and the file Lam_Funs.thy | changeset | files |
| Wed, 01 Nov 2006 15:39:20 +0100 | paulson | More blacklisting | changeset | files |
| Wed, 01 Nov 2006 08:46:54 +0100 | bulwahn | added lexicographic_order tactic | changeset | files |
| Tue, 31 Oct 2006 14:59:27 +0100 | haftmann | new SML serializer | changeset | files |
| Tue, 31 Oct 2006 14:59:26 +0100 | haftmann | clarified make_term interface | changeset | files |
| Tue, 31 Oct 2006 14:58:23 +0100 | haftmann | introduced CodegenData.add_func_legacy | changeset | files |
| Tue, 31 Oct 2006 14:58:16 +0100 | haftmann | cleaned up | changeset | files |
| Tue, 31 Oct 2006 14:58:14 +0100 | haftmann | adapted seralizer syntax | changeset | files |
| Tue, 31 Oct 2006 14:58:12 +0100 | haftmann | adapted to new serializer syntax | changeset | files |
| Tue, 31 Oct 2006 09:29:18 +0100 | haftmann | constructing proof | changeset | files |
| Tue, 31 Oct 2006 09:29:17 +0100 | haftmann | dropped constructiv `-> | changeset | files |
| Tue, 31 Oct 2006 09:29:16 +0100 | haftmann | new serialization syntax; experimental extensions | changeset | files |
| Tue, 31 Oct 2006 09:29:14 +0100 | haftmann | refined | changeset | files |
| Tue, 31 Oct 2006 09:29:13 +0100 | haftmann | refined algorithm | changeset | files |
| Tue, 31 Oct 2006 09:29:12 +0100 | haftmann | simplified preprocessor framework | changeset | files |
| Tue, 31 Oct 2006 09:29:11 +0100 | haftmann | cleanup | changeset | files |
| Tue, 31 Oct 2006 09:29:08 +0100 | haftmann | *** empty log message *** | changeset | files |
| Tue, 31 Oct 2006 09:29:06 +0100 | haftmann | fixed type signature of Type.varify | changeset | files |
| Tue, 31 Oct 2006 09:29:01 +0100 | haftmann | dropped junk | changeset | files |
| Tue, 31 Oct 2006 09:28:57 +0100 | haftmann | disabled some code generation (an intermeidate solution) | changeset | files |