Thu, 05 Apr 2012 10:45:53 +0200 wenzelm tuned;
Wed, 04 Apr 2012 21:03:30 +0200 wenzelm tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
Wed, 04 Apr 2012 17:21:39 +0200 wenzelm proper signature constraint;
Wed, 04 Apr 2012 17:14:19 +0200 wenzelm tuned comments;
Wed, 04 Apr 2012 14:19:47 +0200 wenzelm separate module for prover command execution;
Wed, 04 Apr 2012 14:00:47 +0200 wenzelm tuned;
Wed, 04 Apr 2012 10:38:04 +0200 huffman fix typo in ML structure name
Wed, 04 Apr 2012 11:15:54 +0200 wenzelm removed obsolete isar-overview manual;
Wed, 04 Apr 2012 10:04:25 +0100 sultana dealing with SMLNJ errors 'value type in structure doesn't match signature spec' (which originated from lack of type generalisation) and 'unresolved flex record' wrt tptp_interpret
Wed, 04 Apr 2012 10:49:42 +0200 bulwahn merged
Wed, 04 Apr 2012 10:17:54 +0200 bulwahn rudimentary handling of products in finitize_functions in Quickcheck-Narrowing
Wed, 04 Apr 2012 10:17:08 +0200 bulwahn improved equality check for modes in predicate compiler
Wed, 04 Apr 2012 09:00:10 +0200 huffman rename ML structure to avoid shadowing earlier name
Wed, 04 Apr 2012 07:47:42 +0200 huffman add type annotations to make SML happy (cf. ec6187036495)
Tue, 03 Apr 2012 23:49:24 +0200 huffman merged
Tue, 03 Apr 2012 22:31:00 +0200 huffman new transfer proof method
Tue, 03 Apr 2012 22:04:50 +0200 huffman renamed Tools/transfer.ML to Tools/legacy_transfer.ML
Tue, 03 Apr 2012 21:39:28 +0200 wenzelm prefer prog-prove, suppress isar-overview;
Tue, 03 Apr 2012 21:09:09 +0200 wenzelm merged
Tue, 03 Apr 2012 20:41:13 +0200 wenzelm merged
Tue, 03 Apr 2012 20:42:00 +0200 wenzelm formal integration of "prog-prove" manual;
Tue, 03 Apr 2012 20:37:52 +0200 wenzelm prefer static dependencies;
Tue, 03 Apr 2012 20:56:32 +0200 huffman merged
Tue, 03 Apr 2012 15:15:00 +0200 huffman modernized obsolete old-style theory name with proper new-style underscore
Tue, 03 Apr 2012 17:33:22 +0100 sultana removed use of CharVector in generated parser, to make SMLNJ happy
Tue, 03 Apr 2012 20:24:00 +0200 wenzelm avoid duplicate PIDE markup;
Tue, 03 Apr 2012 20:08:08 +0200 wenzelm less intrusive visibility;
Tue, 03 Apr 2012 19:49:14 +0200 wenzelm more robust re-import wrt. non-HHF assumptions;
Tue, 03 Apr 2012 19:33:46 +0200 wenzelm consider polyml-5.3.0 as "experimental" since it chokes on HOL-Codegenerator_Test, while 5.2.1 happens to work;
Tue, 03 Apr 2012 18:22:14 +0200 wenzelm close context elements via Expression.cert/read_declaration;
Tue, 03 Apr 2012 17:48:16 +0200 wenzelm merged
Tue, 03 Apr 2012 16:45:44 +0100 sultana added me to isatest email list
Tue, 03 Apr 2012 16:26:48 +0200 kuncar new package Lifting - initial commit
Tue, 03 Apr 2012 14:09:37 +0200 huffman add floor/ceiling lemmas suggested by René Thiemann
Tue, 03 Apr 2012 08:55:06 +0200 nipkow made sure that " is shown in tutorial text
Mon, 02 Apr 2012 21:26:46 +0100 Christian Urban merged
Mon, 02 Apr 2012 21:26:07 +0100 Christian Urban tuned proofs
Mon, 02 Apr 2012 20:12:19 +0200 nipkow merged
Mon, 02 Apr 2012 20:12:10 +0200 nipkow towards showing " in the tutorial
Mon, 02 Apr 2012 18:12:53 +0100 Christian Urban tuned proof in order to avoid warning message
Mon, 02 Apr 2012 16:07:24 +0200 huffman remove unnecessary qualifiers on names
Mon, 02 Apr 2012 16:06:24 +0200 huffman add lemma Suc_1
Mon, 02 Apr 2012 14:09:27 +0200 berghofe merged
Mon, 02 Apr 2012 13:58:59 +0200 berghofe Require "For" keyword to be followed by at least one whitespace, to avoid that
Tue, 03 Apr 2012 17:21:33 +0200 wenzelm normalize defs (again, cf. 008b7858f3c0);
Tue, 03 Apr 2012 16:53:32 +0200 wenzelm some context examples;
Tue, 03 Apr 2012 16:51:01 +0200 wenzelm retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;
Tue, 03 Apr 2012 16:49:05 +0200 wenzelm another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);
Tue, 03 Apr 2012 16:27:32 +0200 wenzelm export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);
Tue, 03 Apr 2012 16:10:34 +0200 wenzelm better drop background syntax if entity depends on parameters;
Tue, 03 Apr 2012 14:37:16 +0200 wenzelm more uniform abbrev vs. define;
Tue, 03 Apr 2012 13:47:15 +0200 wenzelm tuned;
Tue, 03 Apr 2012 11:28:21 +0200 wenzelm clarified generic_const vs. close_schematic_term;
Tue, 03 Apr 2012 11:21:17 +0200 wenzelm tuned;
Tue, 03 Apr 2012 10:59:20 +0200 wenzelm more uniform theory_abbrev with const_declaration;
Tue, 03 Apr 2012 10:04:41 +0200 wenzelm avoid const_declaration in aux. context (cf. locale_foundation);
Tue, 03 Apr 2012 09:47:20 +0200 wenzelm clarified background_foundation vs. theory_foundation (with const_declaration);
Tue, 03 Apr 2012 09:41:16 +0200 wenzelm tuned;
Mon, 02 Apr 2012 23:55:25 +0200 wenzelm more general standard_declaration;
Mon, 02 Apr 2012 23:27:24 +0200 wenzelm better restore after close_target;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip