Sun, 05 Nov 2006 21:44:33 +0100 wenzelm fixed print_translation for ALL/EX and <, <=, etc.; tuned syntax names;
Sun, 05 Nov 2006 21:44:32 +0100 wenzelm Sign.const_syntax_name;
Sun, 05 Nov 2006 09:36:25 +0100 haftmann added gfx
Sat, 04 Nov 2006 19:25:43 +0100 wenzelm removed checkpoint interface;
Sat, 04 Nov 2006 19:25:43 +0100 wenzelm String.compare: slow version -- performance test;
Sat, 04 Nov 2006 19:25:41 +0100 wenzelm replaced apply_copy by apply';
Sat, 04 Nov 2006 19:25:41 +0100 wenzelm removed is_Trueprop (use can dest_Trueprop'' instead);
Sat, 04 Nov 2006 19:25:40 +0100 wenzelm removed is_Trueprop (use can dest_Trueprop'' instead);
Sat, 04 Nov 2006 19:25:39 +0100 wenzelm updated;
Sat, 04 Nov 2006 19:25:38 +0100 wenzelm HOL_USEDIR_OPTIONS: -p 1 by default;
Sat, 04 Nov 2006 19:25:36 +0100 wenzelm tuned;
Sat, 04 Nov 2006 19:25:34 +0100 wenzelm * October 2006: Stefan Hohe, TUM;
Sat, 04 Nov 2006 13:19:04 +0100 wenzelm replaced Toplevel.proof_to_theory by Toplevel.end_proof;
Sat, 04 Nov 2006 12:53:35 +0100 wenzelm optional argument for timespan (default 100);
Sat, 04 Nov 2006 12:46:40 +0100 wenzelm added at-mac-poly-e, at64-poly-e;
Sat, 04 Nov 2006 00:12:06 +0100 huffman moved DERIV stuff from Lim.thy to new Deriv.thy; cleaned up LIMSEQ_SEQ proofs
Sat, 04 Nov 2006 00:11:11 +0100 huffman new Deriv.thy contains stuff from Lim.thy
Fri, 03 Nov 2006 15:28:13 +0100 haftmann re-added simpdata.ML
Fri, 03 Nov 2006 14:22:48 +0100 haftmann new ML serializer
Fri, 03 Nov 2006 14:22:47 +0100 haftmann fixed problem with eta-expansion
Fri, 03 Nov 2006 14:22:46 +0100 haftmann tuned
Fri, 03 Nov 2006 14:22:45 +0100 haftmann fixed problem with variable names
Fri, 03 Nov 2006 14:22:44 +0100 haftmann tightened notion of function equations
Fri, 03 Nov 2006 14:22:43 +0100 haftmann dropped name_mangler.ML
Fri, 03 Nov 2006 14:22:42 +0100 haftmann some example tweaking
Fri, 03 Nov 2006 14:22:41 +0100 haftmann added particular test for partially applied case constants
Fri, 03 Nov 2006 14:22:40 +0100 haftmann improved evaluation setup
Fri, 03 Nov 2006 14:22:39 +0100 haftmann adapted to changes in codegen_data.ML
Fri, 03 Nov 2006 14:22:38 +0100 haftmann added code gen II
Fri, 03 Nov 2006 14:22:37 +0100 haftmann simplified reasoning tools setup
Fri, 03 Nov 2006 14:22:36 +0100 haftmann dropped prop_cs
Fri, 03 Nov 2006 14:22:35 +0100 haftmann dropped equals_conv for nbe
Fri, 03 Nov 2006 14:22:34 +0100 haftmann first version of style guide
Fri, 03 Nov 2006 14:22:33 +0100 haftmann continued tutorial
Fri, 03 Nov 2006 14:22:31 +0100 haftmann added serialization keywords
Thu, 02 Nov 2006 14:27:18 +0100 dixon bugfix to zipto: left and right were wrong way around.
Thu, 02 Nov 2006 13:35:09 +0100 nipkow added sum_squared
Wed, 01 Nov 2006 19:07:37 +0100 urbanc changed a misplaced "also" to a "moreover" (caused a loop somehow)
Wed, 01 Nov 2006 19:03:30 +0100 urbanc changed to not compile Iteration and Recursion, but Lam_Funs instead
Wed, 01 Nov 2006 17:57:02 +0100 huffman move DERIV_sumr from Series.thy to Lim.thy
Wed, 01 Nov 2006 17:14:16 +0100 huffman generalize type of lemma isCont_Id
Wed, 01 Nov 2006 16:48:58 +0100 huffman new proof of Bseq_NSbseq using transfer
Wed, 01 Nov 2006 16:11:31 +0100 urbanc changed to use Lam_Funs
Wed, 01 Nov 2006 15:51:11 +0100 paulson clauses for iff-introduction, unfortunately useless
Wed, 01 Nov 2006 15:50:19 +0100 urbanc tuned
Wed, 01 Nov 2006 15:49:43 +0100 paulson Numerous cosmetic changes.
Wed, 01 Nov 2006 15:45:44 +0100 urbanc not needed anymore
Wed, 01 Nov 2006 15:44:31 +0100 urbanc these files are superseded by the internal recursion combinator and the file Lam_Funs.thy
Wed, 01 Nov 2006 15:39:20 +0100 paulson More blacklisting
Wed, 01 Nov 2006 08:46:54 +0100 bulwahn added lexicographic_order tactic
Tue, 31 Oct 2006 14:59:27 +0100 haftmann new SML serializer
Tue, 31 Oct 2006 14:59:26 +0100 haftmann clarified make_term interface
Tue, 31 Oct 2006 14:58:23 +0100 haftmann introduced CodegenData.add_func_legacy
Tue, 31 Oct 2006 14:58:16 +0100 haftmann cleaned up
Tue, 31 Oct 2006 14:58:14 +0100 haftmann adapted seralizer syntax
Tue, 31 Oct 2006 14:58:12 +0100 haftmann adapted to new serializer syntax
Tue, 31 Oct 2006 09:29:18 +0100 haftmann constructing proof
Tue, 31 Oct 2006 09:29:17 +0100 haftmann dropped constructiv `->
Tue, 31 Oct 2006 09:29:16 +0100 haftmann new serialization syntax; experimental extensions
Tue, 31 Oct 2006 09:29:14 +0100 haftmann refined
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip