isabelle: Graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -120 +120 +1000 +3000 +10000 +30000 tip

provide color values via options;
2012-09-11, by wenzelm
prefer tuning parameters as public methods (again) -- to allow overriding in applications;
2012-09-11, by wenzelm
updated keywords;
2012-09-11, by wenzelm
merged
2012-09-11, by wenzelm
tuned;
2012-09-11, by wenzelm
more informative tooltip: default value;
2012-09-11, by wenzelm
more options;
2012-09-11, by wenzelm
allow defaults for one datatype to involve the constructor of another one in the mutually recursive case
2012-09-11, by blanchet
added "defaults" option
2012-09-11, by 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)
2012-09-11, by blanchet
spin off "bnf_def_tactics.ML"
2012-09-11, by blanchet
move "bnf_util.ML" to "BNF_Util.thy"
2012-09-11, by blanchet
renamed "BNF_Library" to "BNF_Util"
2012-09-11, by blanchet
generate all sel theorems
2012-09-11, by blanchet
allow default values for selectors in low-level "wrap_data" command
2012-09-11, by blanchet
removed needless "infer_types" call
2012-09-11, by blanchet
added no_dests option
2012-09-11, by blanchet
tuning
2012-09-11, by blanchet
finished splitting sum types for corecursors
2012-09-11, by blanchet
split sum types in corecursor definition
2012-09-11, by blanchet
first step towards splitting corecursor function arguments into (p, g, h) triples
2012-09-11, by blanchet
reverted "id" change: The problem is rather that the "%c. f c" argument sometimes gets eta-reduced
2012-09-11, by blanchet
replaced jedit_relative_font_size by jedit_font_scale;
2012-09-11, by wenzelm
need to provide label via some jEdit property;
2012-09-11, by wenzelm
some support to organize options in sections;
2012-09-11, by wenzelm
merged
2012-09-11, by wenzelm
generate "id" rather than (%v. v)
2012-09-11, by blanchet
correctly generate sel_coiter and sel_corec theorems
2012-09-11, by blanchet
generate "sel_coiters" and friends
2012-09-10, by blanchet
sanity check
2012-09-10, by blanchet
implemented and use "mk_sum_casesN_balanced"
2012-09-10, by blanchet
fixed general case of "mk_sumEN_balanced"
2012-09-10, by blanchet
debug
2012-09-10, by blanchet
fixed base case of "mk_sumEN_balanced"
2012-09-10, by blanchet
prevent inconsistent selector types
2012-09-10, by blanchet
minor optimization
2012-09-10, by blanchet
allow same selector name for several constructors
2012-09-10, by blanchet
removed done TODO
2012-09-10, by blanchet
avoid type inference + tuning
2012-09-10, by blanchet
use balanced sums for constructors (to gracefully handle 100 constructors or more)
2012-09-10, by blanchet
busted -- let's use more neutral names
2012-09-10, by blanchet
replacing own dummy value by Haskell's Prelude.undefined
2012-09-10, by bulwahn
prefer global default font over IsabelleText of jEdit TextArea;
2012-09-11, by wenzelm
uniform operation on initial delay;
2012-09-11, by wenzelm
option jedit_load_delay;
2012-09-10, by wenzelm
dynamic evaluation of time (e.g. via options);
2012-09-10, by wenzelm
proper multi-line tooltip;
2012-09-10, by wenzelm
more detailed option tooltip;
2012-09-10, by wenzelm
more systematic JEdit_Options.make_component;
2012-09-10, by wenzelm
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
2012-09-10, by wenzelm
formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
2012-09-10, by wenzelm
more explicit indication of legacy features;
2012-09-10, by wenzelm
more explicit indication of legacy features;
2012-09-10, by wenzelm
simplify "Process" example even further
2012-09-10, by traytel
stabilized generation of parameterized theorem
2012-09-10, by traytel
added snippets
2012-09-10, by nipkow
simplify "Process" example further
2012-09-09, by blanchet
simplify "Process" example
2012-09-09, by blanchet
full name of a type as key in bnf table
2012-09-09, by traytel
fixed bug with one-value codatatype "codata 'a dead_foo = A"
2012-09-09, by blanchet
tuning
2012-09-09, by blanchet
fixed and reenabled "corecs" theorems
2012-09-09, by blanchet
fixed and enabled generation of "coiters" theorems, including the recursive case
2012-09-09, by blanchet
generate "fld_unf_corecs" as well
2012-09-09, by blanchet
reactivated generation of "coiters" theorems
2012-09-09, by blanchet
use map_id, not map_id', to allow better composition
2012-09-09, by blanchet
open typedefs everywhere in the package
2012-09-09, by traytel
open typedef for datatypes
2012-09-09, by traytel
fixed and enabled iterator/recursor theorems
2012-09-08, by blanchet
renamed for consistency
2012-09-08, by blanchet
oops
2012-09-08, by blanchet
tuning
2012-09-08, by blanchet
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
2012-09-08, by blanchet
fixed bug with one-value types with phantom type arguments
2012-09-08, by blanchet
imported patch debugging
2012-09-08, by blanchet
repaired "nofail4" example
2012-09-08, by blanchet
renamed xxxBNF to pre_xxx
2012-09-08, by blanchet
fixed handling of map of "fun"
2012-09-08, by blanchet
comment out code that's not ready
2012-09-08, by blanchet
tuning
2012-09-08, by blanchet
construct the right iterator theorem in the recursive case
2012-09-08, by blanchet
some work on coiter tactic
2012-09-08, by blanchet
more sugar on codatatypes
2012-09-08, by blanchet
define corecursors
2012-09-08, by blanchet
define coiterators
2012-09-08, by blanchet
TODO
2012-09-08, by blanchet
tuning
2012-09-08, by blanchet
completed iter/rec proofs
2012-09-08, by blanchet
TODOs
2012-09-08, by blanchet
implemented "mk_iter_or_rec_tac"
2012-09-08, by blanchet
generate iter/rec goals
2012-09-08, by blanchet
repaired constant types
2012-09-08, by blanchet
some work towards iterator and recursor properties
2012-09-08, by blanchet
tuning
2012-09-08, by blanchet
correctly curry recursor arguments
2012-09-08, by blanchet
added high-level recursor, not yet curried
2012-09-08, by blanchet
merged
2012-09-07, by wenzelm
tuned proofs;
2012-09-07, by wenzelm
postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;
2012-09-07, by wenzelm
more explicit Delay operations;
2012-09-07, by wenzelm
tuned proofs;
2012-09-07, by wenzelm
clearer names for functions in Quickcheck's narrowing engine
2012-09-07, by bulwahn
merged
2012-09-07, by nipkow
tuned latex
2012-09-07, by nipkow
lattice instances for option type
2012-09-07, by haftmann
combinator Option.these
2012-09-07, by haftmann
adjusted examples
2012-09-07, by nipkow
countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"
2012-09-06, by huffman
handle type constructors not known to be a BNF using the DEADID BNF
2012-09-06, by traytel
respect order of/additional type variables supplied by the user in fixed point constructions;
2012-09-06, by traytel
gracefully handle shadowing case (fourth step of sugar localization)
2012-09-06, by blanchet
careful about constructor types w.r.t. fake context (third step of localization)
2012-09-06, by blanchet
read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)
2012-09-06, by blanchet
tuning
2012-09-06, by blanchet
use "add_type" rather than "add_types_global"
2012-09-06, by blanchet
don't throw away the context when hacking the theory (first step to localize the sugar code)
2012-09-06, by blanchet
tuning
2012-09-06, by blanchet
introduced and used "mk_Freesss", and simplified "mk_Freess(')"
2012-09-06, by blanchet
construct high-level iterator RHS
2012-09-06, by blanchet
option for discarding build results, enabled in particular for Isabelle_makeall
2012-09-06, by krauss