Tue, 05 Jul 2011 21:53:59 +0200 wenzelm hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
Tue, 05 Jul 2011 21:32:48 +0200 wenzelm prefer space_explode/split_lines as in Isabelle/ML;
Tue, 05 Jul 2011 21:20:24 +0200 wenzelm Path.split convenience;
Tue, 05 Jul 2011 20:36:49 +0200 wenzelm get theory from last executation state;
Tue, 05 Jul 2011 19:45:59 +0200 wenzelm explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
Tue, 05 Jul 2011 11:45:48 +0200 wenzelm clarified cancel_execution/await_cancellation;
Tue, 05 Jul 2011 11:16:37 +0200 wenzelm tuned signature;
Tue, 05 Jul 2011 10:54:05 +0200 wenzelm tuned;
Tue, 05 Jul 2011 09:54:39 +0200 krauss re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
Mon, 04 Jul 2011 22:25:33 +0200 wenzelm Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
Mon, 04 Jul 2011 22:11:32 +0200 wenzelm quasi-static Isabelle_System -- reduced tendency towards "functorial style";
Mon, 04 Jul 2011 20:18:19 +0200 wenzelm explicit class Counter;
Mon, 04 Jul 2011 16:54:58 +0200 wenzelm merged
Mon, 04 Jul 2011 10:23:46 +0200 hoelzl the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
Mon, 04 Jul 2011 10:15:49 +0200 hoelzl equalities of subsets of atLeastLessThan
Sun, 03 Jul 2011 09:59:25 +0200 bulwahn adding documentation of the value antiquotation to the code generation manual
Sun, 03 Jul 2011 08:15:14 +0200 blanchet make SML/NJ happy
Sat, 02 Jul 2011 22:55:58 +0200 haftmann install case certificate for If after code_datatype declaration for bool
Sat, 02 Jul 2011 22:14:47 +0200 haftmann tuned typo
Mon, 04 Jul 2011 16:51:45 +0200 wenzelm pervasive Basic_Library in Scala;
Mon, 04 Jul 2011 16:27:11 +0200 wenzelm some support for theory files within Isabelle/Scala session;
Mon, 04 Jul 2011 13:43:10 +0200 wenzelm imitate exception ERROR of Isabelle/ML;
Sun, 03 Jul 2011 19:53:35 +0200 wenzelm eliminated null;
Sun, 03 Jul 2011 19:42:32 +0200 wenzelm more explicit edit_node vs. init_node;
Sun, 03 Jul 2011 15:10:17 +0200 wenzelm tuned signature;
Sat, 02 Jul 2011 23:31:07 +0200 wenzelm Thy_Header.read convenience;
Sat, 02 Jul 2011 23:04:19 +0200 wenzelm some support for Session.File_Store;
Sat, 02 Jul 2011 21:24:19 +0200 wenzelm tuned signature;
Sat, 02 Jul 2011 20:54:38 +0200 wenzelm eliminated redundant session_ready;
Sat, 02 Jul 2011 20:22:02 +0200 wenzelm tuned;
Sat, 02 Jul 2011 19:22:06 +0200 wenzelm uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;
Sat, 02 Jul 2011 19:08:51 +0200 wenzelm misc tuning;
Sat, 02 Jul 2011 10:37:35 +0200 haftmann correction: do not assume that case const index covered all cases
Fri, 01 Jul 2011 23:31:23 +0200 haftmann remove illegal case combinators after merge
Fri, 01 Jul 2011 23:10:27 +0200 haftmann corrected misunderstanding what `old functions` are supposed to be
Fri, 01 Jul 2011 23:07:06 +0200 haftmann centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be
Fri, 01 Jul 2011 22:48:05 +0200 haftmann merged
Fri, 01 Jul 2011 19:57:41 +0200 haftmann index cases for constructors
Fri, 01 Jul 2011 19:42:07 +0200 noschinl cover induct's "arbitrary" more deeply
Fri, 01 Jul 2011 18:11:17 +0200 wenzelm merged;
Fri, 01 Jul 2011 17:44:04 +0200 blanchet enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
Fri, 01 Jul 2011 16:31:33 +0200 blanchet made minimizer informative output accurate
Fri, 01 Jul 2011 15:53:38 +0200 blanchet test a few more type encodings
Fri, 01 Jul 2011 15:53:38 +0200 blanchet further repair "mangled_tags", now that tags are also mangled
Fri, 01 Jul 2011 15:53:38 +0200 blanchet update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
Fri, 01 Jul 2011 15:53:38 +0200 blanchet renamed "type_sys" to "type_enc", which is more accurate
Fri, 01 Jul 2011 15:53:37 +0200 blanchet document "simple_higher" type encoding
Fri, 01 Jul 2011 15:53:37 +0200 blanchet cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
Fri, 01 Jul 2011 15:53:37 +0200 blanchet mangle "ti" tags
Fri, 01 Jul 2011 15:53:37 +0200 blanchet tuning
Fri, 01 Jul 2011 17:36:25 +0200 wenzelm clarified Thy_Syntax.element;
Fri, 01 Jul 2011 16:05:38 +0200 wenzelm tuned layout;
Fri, 01 Jul 2011 15:16:03 +0200 wenzelm proper @{binding} antiquotations (relevant for formal references);
Fri, 01 Jul 2011 15:14:44 +0200 wenzelm tuned;
Fri, 01 Jul 2011 14:17:02 +0200 wenzelm merged
Fri, 01 Jul 2011 13:54:25 +0200 noschinl reverted 782991e4180d: fold_fields was never used
Fri, 01 Jul 2011 13:54:23 +0200 noschinl reverted ce00462f,b3759dce, 7a165592: unwanted generalisation
Fri, 01 Jul 2011 11:26:02 +0200 bulwahn improving actual dependencies
Fri, 01 Jul 2011 10:45:51 +0200 bulwahn adding a minimalistic documentation of the value antiquotation in the Isar reference manual
Fri, 01 Jul 2011 10:45:49 +0200 bulwahn adding a value antiquotation
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip