Tue, 11 Sep 2012 18:12:23 +0200 blanchet removed wrong "transpose" and ensure "sel" theorems are put in the right order (grouped per selector, in the order in which the selectors appear)
Tue, 11 Sep 2012 17:36:09 +0200 blanchet spin off "bnf_def_tactics.ML"
Tue, 11 Sep 2012 17:14:49 +0200 blanchet move "bnf_util.ML" to "BNF_Util.thy"
Tue, 11 Sep 2012 17:09:39 +0200 blanchet renamed "BNF_Library" to "BNF_Util"
Tue, 11 Sep 2012 17:06:27 +0200 blanchet generate all sel theorems
Tue, 11 Sep 2012 16:08:55 +0200 blanchet allow default values for selectors in low-level "wrap_data" command
Tue, 11 Sep 2012 16:08:27 +0200 blanchet removed needless "infer_types" call
Tue, 11 Sep 2012 14:51:52 +0200 blanchet added no_dests option
Tue, 11 Sep 2012 13:10:34 +0200 blanchet tuning
Tue, 11 Sep 2012 13:06:14 +0200 blanchet finished splitting sum types for corecursors
Tue, 11 Sep 2012 13:06:14 +0200 blanchet split sum types in corecursor definition
Tue, 11 Sep 2012 13:06:13 +0200 blanchet first step towards splitting corecursor function arguments into (p, g, h) triples
Tue, 11 Sep 2012 13:06:13 +0200 blanchet reverted "id" change: The problem is rather that the "%c. f c" argument sometimes gets eta-reduced
Tue, 11 Sep 2012 16:10:54 +0200 wenzelm replaced jedit_relative_font_size by jedit_font_scale;
Tue, 11 Sep 2012 15:59:35 +0200 wenzelm need to provide label via some jEdit property;
Tue, 11 Sep 2012 15:47:42 +0200 wenzelm some support to organize options in sections;
Tue, 11 Sep 2012 11:53:34 +0200 wenzelm merged
Tue, 11 Sep 2012 09:40:05 +0200 blanchet generate "id" rather than (%v. v)
Tue, 11 Sep 2012 09:40:05 +0200 blanchet correctly generate sel_coiter and sel_corec theorems
Mon, 10 Sep 2012 21:44:43 +0200 blanchet generate "sel_coiters" and friends
Mon, 10 Sep 2012 18:50:27 +0200 blanchet sanity check
Mon, 10 Sep 2012 18:29:55 +0200 blanchet implemented and use "mk_sum_casesN_balanced"
Mon, 10 Sep 2012 17:52:01 +0200 blanchet fixed general case of "mk_sumEN_balanced"
Mon, 10 Sep 2012 17:36:02 +0200 blanchet debug
Mon, 10 Sep 2012 17:36:02 +0200 blanchet fixed base case of "mk_sumEN_balanced"
Mon, 10 Sep 2012 17:36:02 +0200 blanchet prevent inconsistent selector types
Mon, 10 Sep 2012 17:36:02 +0200 blanchet minor optimization
Mon, 10 Sep 2012 17:36:02 +0200 blanchet allow same selector name for several constructors
Mon, 10 Sep 2012 17:36:02 +0200 blanchet removed done TODO
Mon, 10 Sep 2012 17:36:02 +0200 blanchet avoid type inference + tuning
Mon, 10 Sep 2012 17:35:53 +0200 blanchet use balanced sums for constructors (to gracefully handle 100 constructors or more)
Mon, 10 Sep 2012 17:32:39 +0200 blanchet busted -- let's use more neutral names
Mon, 10 Sep 2012 14:52:22 +0200 bulwahn replacing own dummy value by Haskell's Prelude.undefined
Tue, 11 Sep 2012 11:29:28 +0200 wenzelm prefer global default font over IsabelleText of jEdit TextArea;
Tue, 11 Sep 2012 11:03:59 +0200 wenzelm uniform operation on initial delay;
Mon, 10 Sep 2012 21:17:32 +0200 wenzelm option jedit_load_delay;
Mon, 10 Sep 2012 21:15:46 +0200 wenzelm dynamic evaluation of time (e.g. via options);
Mon, 10 Sep 2012 19:56:08 +0200 wenzelm proper multi-line tooltip;
Mon, 10 Sep 2012 19:49:30 +0200 wenzelm more detailed option tooltip;
Mon, 10 Sep 2012 17:13:17 +0200 wenzelm more systematic JEdit_Options.make_component;
Mon, 10 Sep 2012 15:20:50 +0200 wenzelm manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
Mon, 10 Sep 2012 13:19:56 +0200 wenzelm formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
Mon, 10 Sep 2012 12:13:39 +0200 wenzelm more explicit indication of legacy features;
Mon, 10 Sep 2012 12:00:28 +0200 wenzelm more explicit indication of legacy features;
Mon, 10 Sep 2012 09:57:21 +0200 traytel simplify "Process" example even further
Mon, 10 Sep 2012 09:56:06 +0200 traytel stabilized generation of parameterized theorem
Mon, 10 Sep 2012 06:46:17 +0200 nipkow added snippets
Sun, 09 Sep 2012 21:22:31 +0200 blanchet simplify "Process" example further
Sun, 09 Sep 2012 21:22:31 +0200 blanchet simplify "Process" example
Sun, 09 Sep 2012 21:13:15 +0200 traytel full name of a type as key in bnf table
Sun, 09 Sep 2012 19:57:20 +0200 blanchet fixed bug with one-value codatatype "codata 'a dead_foo = A"
Sun, 09 Sep 2012 19:05:53 +0200 blanchet tuning
Sun, 09 Sep 2012 18:55:10 +0200 blanchet fixed and reenabled "corecs" theorems
Sun, 09 Sep 2012 17:14:39 +0200 blanchet fixed and enabled generation of "coiters" theorems, including the recursive case
Sun, 09 Sep 2012 13:04:57 +0200 blanchet generate "fld_unf_corecs" as well
Sun, 09 Sep 2012 12:51:17 +0200 blanchet reactivated generation of "coiters" theorems
Sun, 09 Sep 2012 12:07:15 +0200 blanchet use map_id, not map_id', to allow better composition
Sun, 09 Sep 2012 10:58:11 +0200 traytel open typedefs everywhere in the package
Sun, 09 Sep 2012 10:15:58 +0200 traytel open typedef for datatypes
Sat, 08 Sep 2012 22:54:37 +0200 blanchet fixed and enabled iterator/recursor theorems
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip