isabelle: Graph

alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
2012-09-16, by wenzelm
got rid of ad-hoc lift function
2012-09-16, by nipkow
converted wt into a set, tuned names
2012-09-16, by nipkow
use strip_typeN in bnf_def (instead of repairing strip_type)
2012-09-16, by traytel
removing find_theorems commands that were left in the developments accidently
2012-09-16, by bulwahn
tuning
2012-09-15, by blanchet
tuned code to avoid special case for "fun"
2012-09-15, by blanchet
tuned induction tactic
2012-09-15, by blanchet
tuned error message
2012-09-15, by blanchet
tuning
2012-09-15, by blanchet
typeclass formalising bounded subtraction
2012-09-15, by haftmann
dropped some unused identifiers
2012-09-15, by haftmann
export rel_mono theorem
2012-09-15, by traytel
merged two unfold steps
2012-09-14, by blanchet
took out one rotate_tac
2012-09-14, by blanchet
killed spurious rotate_tac; use auto instead of blast
2012-09-14, by blanchet
moved blast tactic to where it is actually needed
2012-09-14, by blanchet
fixed bug in "mk_map" for the "fun" case
2012-09-14, by blanchet
correct generalization to 3 or more mutually recursive datatypes
2012-09-14, by blanchet
provide more guidance, exploiting our knowledge of the goal
2012-09-14, by blanchet
fixed issue with bound variables in prem prems + tuning
2012-09-14, by blanchet
use right version of "mk_UnIN"
2012-09-14, by blanchet
select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking
2012-09-14, by blanchet
tuned code before fixing "mk_induct_discharge_prem_prems_tac"
2012-09-14, by blanchet
tuned proofs;
2012-09-14, by wenzelm
merged
2012-09-14, by wenzelm
polished the induction
2012-09-14, by blanchet
put the flat at the right place (to avoid exceptions)
2012-09-14, by blanchet
fixed variable exporting problem
2012-09-14, by blanchet
compile
2012-09-14, by blanchet
added induct tactic
2012-09-14, by blanchet
tuning
2012-09-14, by blanchet
renamed "mk_UnN" to "mk_UnIN"
2012-09-14, by blanchet
merged two commands
2012-09-14, by blanchet
allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
2012-09-14, by blanchet
distinguish between nested and nesting BNFs
2012-09-14, by blanchet
make tactic more robust in the case where "asm_simp_tac" already finishes the job
2012-09-14, by blanchet
derive induction via backward proof, to ensure that the premises are in the right order for constructors like "X x y x" where x and y are mutually recursive
2012-09-14, by blanchet
no longer react on global_settings (cf. 34ac36642a31);
2012-09-14, by wenzelm
refined output panel: more value-oriented approach to update and caret focus;
2012-09-14, by wenzelm
clarified markup names;
2012-09-14, by wenzelm
more general Document_Model.point_range;
2012-09-14, by wenzelm
more static handling of rendering options;
2012-09-14, by wenzelm
tuned options (again);
2012-09-14, by wenzelm
more scalable option-group;
2012-09-14, by wenzelm
tuned
2012-09-14, by nipkow
merged
2012-09-13, by wenzelm
tuned proofs;
2012-09-13, by wenzelm
remove theory Real_Integration, not needed since 44e42d392c6e when Euclidean spaces where introduced
2012-09-13, by hoelzl
workaround for HOL-Mirabelle-ex oddities;
2012-09-13, by wenzelm
instructions for quick start in 20min;
2012-09-13, by wenzelm
more liberal init_components: base dir may get created later when resolving missing components;
2012-09-13, by wenzelm
more efficient painting based on cached result;
2012-09-13, by wenzelm
more standard init_components -- particularly important to pick up correct jdk/scala version;
2012-09-13, by wenzelm
tuned
2012-09-13, by nipkow
merged
2012-09-12, by wenzelm
rough and ready induction
2012-09-12, by blanchet
nicer error message, indicating which type is empty (relying on metatheoretical completeness proof here)
2012-09-12, by blanchet
observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
2012-09-12, by wenzelm
eliminated some old material that is unused in the visible universe;
2012-09-12, by wenzelm
tuning
2012-09-12, by blanchet
set up things for (co)induction sugar
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
added sumEN_tupled_balanced
2012-09-12, by blanchet
load fonts into JavaFX as well;
2012-09-12, by wenzelm
some support for actual HTML rendering;
2012-09-12, by wenzelm
merged
2012-09-12, by wenzelm
free variable name tuning
2012-09-12, by blanchet
reuse generated names (they look better + slightly more efficient)
2012-09-12, by blanchet
desambiguate grammar (e.g. for Nil's mixfix ("[]"))
2012-09-12, by blanchet
avoided duplicate lemma
2012-09-12, by blanchet
put an underscore between names, for compatibility with old package (and also because it makes sense)
2012-09-12, by blanchet
got rid of metis calls
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
2012-09-12, by wenzelm
standardized ML aliases;
2012-09-12, by wenzelm
tuned headers;
2012-09-12, by wenzelm
avoid spaces in markup names, which might cause problems in boundary situations (e.g. HTML class);
2012-09-12, by wenzelm
discontinued experiment with literal replacement text in PDF (cf. b646316f8b3c, 2ff10e613689);
2012-09-12, by wenzelm
more robust interrupt handling;
2012-09-12, by wenzelm
some attempts to synchronize ROOT/files and document/build;
2012-09-12, by wenzelm
tuned error;
2012-09-12, by wenzelm
option_pred characterization
2012-09-12, by traytel
true vs. True in pattern matching
2012-09-12, by traytel
reduced theory dependencies
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
moved theorems closer to where they are used
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
renamed "Ordinals_and_Cardinals" to "Cardinals"
2012-09-12, by blanchet
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
2012-09-12, by blanchet
reorganized dependencies so that the sugar does not depend on GFP -- this will be essential for bootstrapping
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
tuning annotations
2012-09-12, by blanchet
tuned antiquotations
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
tuning
2012-09-12, by blanchet
added optional qualifiers for constructors and destructors, similarly to the old package
2012-09-12, by blanchet
adapted example
2012-09-12, by blanchet
added attributes to theorems
2012-09-12, by blanchet
merged
2012-09-11, by wenzelm
support for sort constraints in new (co)data commands
2012-09-11, by blanchet
provide a programmatic interface for FP sugar
2012-09-11, by blanchet
some GUI support for color options;
2012-09-11, by wenzelm
more precise sections;
2012-09-11, by wenzelm
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