Thu, 23 Sep 2010 13:23:22 +0200 haftmann reverted cs 07549694e2f1 -- use re-printing with current print mode instead after code assembly, avoid Latex.output_typewriter
Thu, 23 Sep 2010 13:23:21 +0200 haftmann reverted cs 07549694e2f1
Thu, 23 Sep 2010 11:29:22 +0200 haftmann shifted abstraction over imperative print mode
Thu, 23 Sep 2010 17:22:45 +0200 bulwahn removing unneccessary expansion procedure for elimination rules; removing obsolete elim preprocessing; tuned
Thu, 23 Sep 2010 17:22:44 +0200 bulwahn moving the preprocessing of introduction rules after the code_pred command; added tuple expansion preprocessing of elimination rule
Thu, 23 Sep 2010 14:50:18 +0200 bulwahn exporting the generic version instead of the context version in quickcheck
Thu, 23 Sep 2010 14:50:18 +0200 bulwahn splitting Predicate_Compile_Examples into Examples and Predicate_Compile_Tests
Thu, 23 Sep 2010 14:50:17 +0200 bulwahn adding a mutual recursive example for named alternative rules for the predicate compiler
Thu, 23 Sep 2010 14:50:16 +0200 bulwahn handling TYPE_MATCH error by raising user error message if user gives introduction rules with mismatching types
Thu, 23 Sep 2010 14:50:16 +0200 bulwahn improving naming of assumptions in code_pred
Thu, 23 Sep 2010 14:50:15 +0200 bulwahn adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim
Thu, 23 Sep 2010 14:50:14 +0200 bulwahn handling equivalences smarter in the predicate compiler
Thu, 23 Sep 2010 14:50:14 +0200 bulwahn removing duplicate rewrite rule from simpset in predicate compiler
Thu, 23 Sep 2010 14:50:13 +0200 bulwahn rewriting function mk_Eval_of in predicate compiler
Thu, 23 Sep 2010 10:39:25 +0200 haftmann merged
Thu, 23 Sep 2010 10:37:28 +0200 haftmann improved and tuned external codegen tool
Thu, 23 Sep 2010 10:34:01 +0200 blanchet make SML/NJ happy
Thu, 23 Sep 2010 09:53:52 +0200 haftmann CONTRIBUTORS and NEWS
Thu, 23 Sep 2010 08:30:33 +0200 haftmann corrections and tuning
Wed, 22 Sep 2010 18:40:35 +0200 haftmann merged
Wed, 22 Sep 2010 18:40:23 +0200 haftmann merged
Wed, 22 Sep 2010 17:11:27 +0200 haftmann merged
Wed, 22 Sep 2010 12:22:47 +0200 haftmann tuned
Fri, 24 Sep 2010 14:47:01 +0200 wenzelm persistent session-panel.selection;
Fri, 24 Sep 2010 14:14:21 +0200 wenzelm slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
Fri, 24 Sep 2010 14:12:33 +0200 wenzelm permissive exit;
Fri, 24 Sep 2010 00:00:21 +0200 wenzelm added Session_Dockable.session_phase label;
Thu, 23 Sep 2010 23:04:50 +0200 wenzelm separate Plugin.init_model;
Thu, 23 Sep 2010 22:04:18 +0200 wenzelm simplified Session.Phase;
Thu, 23 Sep 2010 22:00:36 +0200 wenzelm tuned messages -- cf. Admin/MacOS/App1;
Thu, 23 Sep 2010 20:34:05 +0200 wenzelm tuned dialog;
Thu, 23 Sep 2010 18:44:26 +0200 wenzelm explicit Session.Phase indication with associated event bus;
Thu, 23 Sep 2010 16:48:48 +0200 wenzelm tuned signature;
Thu, 23 Sep 2010 16:48:12 +0200 wenzelm Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
Thu, 23 Sep 2010 15:36:03 +0200 wenzelm tuned;
Thu, 23 Sep 2010 15:21:04 +0200 wenzelm manage persistent syslog via Session, not Isabelle_Process;
Thu, 23 Sep 2010 14:39:29 +0200 wenzelm tuned prover message categorization;
Thu, 23 Sep 2010 14:26:55 +0200 wenzelm tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;
Thu, 23 Sep 2010 13:28:19 +0200 wenzelm tuned message;
Wed, 22 Sep 2010 22:39:17 +0200 wenzelm Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
Wed, 22 Sep 2010 22:25:21 +0200 wenzelm Snapshot.convert/revert: explicit error report to isolate sporadic crash;
Wed, 22 Sep 2010 22:15:36 +0200 wenzelm make compiler doubly sure;
Wed, 22 Sep 2010 22:14:25 +0200 wenzelm isabelle-process: less verbose no-commit mode;
Wed, 22 Sep 2010 21:21:04 +0200 wenzelm tuned message;
Wed, 22 Sep 2010 20:50:25 +0200 wenzelm tuned panel names and actions;
Wed, 22 Sep 2010 18:21:48 +0200 wenzelm renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
Wed, 22 Sep 2010 17:46:59 +0200 wenzelm reactivated polyml-5.4.0 -- SVN 1214 fixes a problem with arbitrary precision arithmetic that was triggered by method "approximation" in HOL/Decision_Procs/Approximation_Ex.thy;
Wed, 22 Sep 2010 16:52:21 +0200 nipkow merged
Wed, 22 Sep 2010 16:52:09 +0200 nipkow more lists lemmas
Wed, 22 Sep 2010 16:24:41 +0200 wenzelm merged
Wed, 22 Sep 2010 11:46:28 +0200 haftmann merged
Wed, 22 Sep 2010 10:30:24 +0200 haftmann tuned text
Wed, 22 Sep 2010 10:22:50 +0200 haftmann sections on @{code} and code_reflect
Wed, 22 Sep 2010 10:04:17 +0200 haftmann formal syntax diagram for code_reflect
Wed, 22 Sep 2010 09:40:11 +0200 haftmann distinguish SML and Eval explicitly
Tue, 21 Sep 2010 15:46:06 +0200 haftmann no_frees_* is subsumed by new framework mechanisms in Code_Preproc
Tue, 21 Sep 2010 15:46:06 +0200 haftmann reject term variables explicitly
Tue, 21 Sep 2010 15:46:05 +0200 haftmann avoid frees and vars in terms to be evaluated by abstracting and applying
Tue, 21 Sep 2010 15:46:05 +0200 haftmann tuned whitespace
Wed, 22 Sep 2010 10:02:39 +0200 blanchet make SML/NJ happier
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip