Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
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
by default, only generate one discriminator for a two-value datatype
2012-09-05, by blanchet
eliminated potentially confusing terminology of Scala "layer";
2012-09-05, by wenzelm
merged
2012-09-05, by wenzelm
tuned proofs;
2012-09-05, by wenzelm
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
2012-09-05, by wenzelm
honor mixfix specifications
2012-09-05, by blanchet
code indentation
2012-09-05, by blanchet
print timing information
2012-09-05, by blanchet
adapted example
2012-09-05, by blanchet
check type variables on rhs
2012-09-05, by blanchet
proper subsexp projection of Isabelle_Markup.Path, in correspondence to 5d0cd770828e;
2012-09-05, by wenzelm
added tooltip to reveal jEdit platform file name;
2012-09-05, by wenzelm
commented out slow examples again
2012-09-05, by blanchet
fixed (n + 1)st bug in "mk_exhaust_tac" -- arose with uncurried constructors
2012-09-05, by blanchet
fixed "mk_exhaust_tac" for the nth time
2012-09-05, by blanchet
updated README
2012-09-05, by blanchet
ported "Misc_Codata" to new syntax
2012-09-05, by blanchet
ported "Misc_Data" to new syntax
2012-09-05, by blanchet
error message only in case of an error
2012-09-05, by traytel
do not trivialize important internal theorem in quick_and_dirty mode
2012-09-05, by traytel
merged
2012-09-05, by wenzelm
made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation)
2012-09-05, by blanchet
tuning (systematic 1-based indices)
2012-09-05, by blanchet
reindented code
2012-09-05, by blanchet
added TODO
2012-09-05, by blanchet
tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it
2012-09-05, by blanchet
fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case
2012-09-05, by blanchet
don't get confused by extraneous premisses
2012-09-05, by blanchet
added a check
2012-09-05, by blanchet
NEWS; CONTRIBUTORS
2012-09-04, by Christian Sternagel
misc tuning;
2012-09-05, by wenzelm
no need to wait 3h on macbroy30 (unlike former macbroy6, cf. 6e5b994070c1);
2012-09-05, by wenzelm
more conservative rechecking of processed constraints in subtyping constraint simplification
2012-09-05, by traytel
added comment for Dmitriy
2012-09-05, by blanchet
fixed bug in type instantiation of case theorem
2012-09-05, by blanchet
use empty binding rather than "*" for default
2012-09-05, by blanchet
tuned
2012-09-05, by nipkow
fixed bugs in one-constructor case
2012-09-05, by blanchet
smoothly handle one-constructor types
2012-09-04, by blanchet
fixed some type issues in sugar "exhaust_tac"
2012-09-04, by blanchet
optionally provide extra dead variables to the FP constructions
2012-09-04, by blanchet
merged
2012-09-04, by wenzelm
added robustness
2012-09-04, by blanchet
added build option -R;
2012-09-04, by wenzelm
implemented "mk_case_tac" -- and got rid of "cheat_tac"
2012-09-04, by blanchet
define "case" constant
2012-09-04, by blanchet
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
2012-09-04, by blanchet
implemented "mk_half_distinct_tac"
2012-09-04, by blanchet
implemented "mk_inject_tac"
2012-09-04, by blanchet
implemented "mk_exhaust_tac"
2012-09-04, by blanchet
more work on FP sugar
2012-09-04, by blanchet
more work on sugar + simplify Trueprop + eq idiom everywhere
2012-09-04, by blanchet
renamed "disc_exclus" theorem to "disc_exclude"
2012-09-04, by blanchet
more work on FP sugar
2012-09-04, by blanchet
smarter "*" syntax -- fallback on "_" if "*" is impossible
2012-09-04, by blanchet
more work on FP sugar
2012-09-04, by blanchet
renamed theorem
2012-09-04, by blanchet
tuned TODO comment
2012-09-04, by blanchet
allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)
2012-09-04, by blanchet
removed oddities
2012-09-04, by blanchet
allow "*" to indicate no discriminator
2012-09-04, by blanchet
tuned TODOs
2012-09-04, by blanchet
started work on sugared "(co)data" commands
2012-09-04, by blanchet
export "wrap" function
2012-09-04, by blanchet
eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)
2012-09-04, by traytel
no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;
2012-09-04, by traytel
enable parallel terminal proofs in interaction;
2012-09-04, by wenzelm
misc tuning;
2012-09-03, by wenzelm
merged
2012-09-03, by wenzelm
killed internal output
2012-09-03, by traytel
generate coinductive witnesses for codatatypes
2012-09-03, by traytel
generalized signature
2012-09-03, by traytel
added examples for testing of coinductive witnesses
2012-09-03, by traytel
continue with more robust dummy session after failed startup;
2012-09-03, by wenzelm
prefer old startup dialog scheme (cf. 514bb82514df);
2012-09-03, by wenzelm
more permissive handling of plugin startup failure;
2012-09-03, by wenzelm
bypass slow check for inlined files, where it is not really required;
2012-09-03, by wenzelm
more direct access to all-important chunks for text painting;
2012-09-03, by wenzelm
merged
2012-09-03, by nipkow
added annotations after condition in if and while
2012-09-03, by nipkow
merge, resolving trivial conflict;
2012-09-03, by wenzelm
forgot to add lemmas
2012-08-30, by Christian Sternagel
hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI
2012-08-30, by Christian Sternagel
reverted (accidentally commited) changes from changeset fd4aef9bc7a9
2012-08-30, by Christian Sternagel
reverted (accidentally commited) changes from changeset fd4aef9bc7a9
2012-08-30, by Christian Sternagel
added theory instantiating type class order for list prefixes
2012-08-30, by Christian Sternagel
Main is implicitly imported via Sublist
2012-08-30, by Christian Sternagel
added author
2012-08-30, by Christian Sternagel
List is implicitly imported by Main
2012-08-30, by Christian Sternagel
introduced "sub" as abbreviation for "emb (op =)";
2012-08-29, by Christian Sternagel
base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)
2012-08-29, by Christian Sternagel
dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)
2012-08-29, by Christian Sternagel
more lemmas on suffixes and embedding
2012-08-29, by Christian Sternagel
changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)
2012-08-29, by Christian Sternagel
added embedding for lists (constant emb)
2012-08-29, by Christian Sternagel
renamed (in Sublist): postfix ~> suffixeq, and dropped infix syntax >>=
2012-08-29, by Christian Sternagel
renamed (in Sublist): prefix ~> prefixeq, strict_prefix ~> prefix
2012-08-29, by Christian Sternagel
renamed theory List_Prefix into Sublist (since it is not only about prefixes)
2012-08-29, by Christian Sternagel
compile
2012-09-03, by blanchet
rearrange dependencies
2012-09-03, by blanchet
renamed three BNF/(co)datatype-related commands
2012-09-03, by blanchet
tuned boundary cases of command-line;
2012-09-03, by wenzelm
"isabelle logo" produces EPS and PDF format simultaneously;
2012-09-03, by wenzelm
actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);
2012-09-03, by wenzelm
tuned proofs;
2012-09-03, by wenzelm
some parallel ML;
2012-09-03, by wenzelm
proper classpath on windows;
2012-09-02, by wenzelm
proper classpath for Java FX;
2012-09-02, by wenzelm
basic setup for HTML5 panel;
2012-09-02, by wenzelm
basic support for Java FX;
2012-09-02, by wenzelm
maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
2012-09-02, by wenzelm
removed unused material;
2012-09-01, by wenzelm
discontinued complicated/unreliable notion of recent proofs within context;
2012-09-01, by wenzelm
central management of forked goals wrt. transaction id;
2012-09-01, by wenzelm
merged
2012-08-31, by wenzelm
always register proofs, even for empty binding;
2012-08-31, by wenzelm
tuned signature;
2012-08-31, by wenzelm
made parser a bit more flexible
2012-08-31, by blanchet
tuning
2012-08-31, by blanchet
pad the selectors' list with default names
2012-08-31, by blanchet
generate default names for selectors
2012-08-31, by blanchet
renamed "disc_disjoint" property "disj_exclus"
2012-08-31, by blanchet
optimized "mk_split_tac" + use "notes"
2012-08-31, by blanchet
optimized "mk_case_disc_tac" further
2012-08-31, by blanchet
optimized "mk_case_disc_tac"
2012-08-31, by blanchet
tuning
2012-08-31, by blanchet
rationalized data structure for distinctness theorems
2012-08-31, by blanchet
optimized "case_cong" proof
2012-08-31, by blanchet
allow default names for selectors via wildcard (_) + fix wrong index (k)
2012-08-31, by blanchet
minor fixes (for compatibility with existing datatype package)
2012-08-31, by blanchet
generate "split_asm" property
2012-08-31, by blanchet
generate "split" property
2012-08-31, by blanchet
more precise register_proofs for local goals;
2012-08-31, by wenzelm
more informative error message from failed goal forks (violating old-style TTY protocol!);
2012-08-31, by wenzelm
avoid empty tooltips;
2012-08-31, by wenzelm
clarified command status (again);
2012-08-31, by wenzelm
recovered ScrollPane from d899be1cfe6d;
2012-08-31, by wenzelm
more markup for failed goal forks, reusing "bad";
2012-08-31, by wenzelm
further refinement of command status, to accomodate forked proofs;
2012-08-31, by wenzelm
merged;
2012-08-30, by wenzelm
make parallel list indexing possible for inject theorems
2012-08-30, by blanchet
generate "weak_case_cong" property
2012-08-30, by blanchet
generate "case_cong" property
2012-08-30, by blanchet
generate "case_disc" property
2012-08-30, by blanchet
generate "ctr_sels" theorems
2012-08-30, by blanchet
generate "disc_exhaust" property
2012-08-30, by blanchet
generate "disc_distinct" theorems
2012-08-30, by blanchet
added discriminator theorems
2012-08-30, by blanchet
adjust example
2012-08-30, by blanchet
more work on sugar
2012-08-30, by blanchet
updated Java-related error message
2012-08-30, by blanchet
changed order of arguments to "bnf_sugar"
2012-08-30, by blanchet
define selectors and discriminators
2012-08-30, by blanchet
tuning
2012-08-30, by blanchet
more work on BNF sugar -- up to derivation of nchotomy
2012-08-30, by blanchet
more work on BNF sugar
2012-08-30, by blanchet
renamed ML function for consistency
2012-08-30, by blanchet
started work on datatype sugar
2012-08-30, by blanchet
killed obsolete "bnf_of_typ" command
2012-08-30, by blanchet
removed dead code
2012-08-30, by blanchet
have "bnf_of_typ" command seal the BNF
2012-08-30, by blanchet
register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;
2012-08-30, by wenzelm
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
2012-08-30, by wenzelm
some support for registering forked proofs within Proof.state, using its bottom context;
2012-08-30, by wenzelm
tuned signature;
2012-08-30, by wenzelm
refined status of forked goals;
2012-08-30, by wenzelm
proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);
2012-08-30, by wenzelm
tuned message;
2012-08-29, by wenzelm
discontinued old init_components script, superseded by init_components shell function as explained in README_REPOSITORY;
2012-08-29, by wenzelm
approximative build of pdf documents in 1 pass instead of 3;
2012-08-29, by wenzelm
more formal isabelle makedist from repository;
2012-08-29, by wenzelm
removed remains of generated material, which tends to rot;
2012-08-29, by wenzelm
one more round to ensure that base images are already there, without producing document output themselves;
2012-08-29, by wenzelm
more robust document setup;
2012-08-29, by wenzelm
provide polyml-5.4.1 as regular component;
2012-08-29, by wenzelm
clarified handling of raw output messages;
2012-08-29, by wenzelm
no attempt to build documentation for now -- requires ML_HOME etc. which is not present here;
2012-08-29, by wenzelm
command 'use' is legacy;
2012-08-29, by wenzelm
clarified separated_chunks vs. space_explode;
2012-08-29, by wenzelm
more precise indentation;
2012-08-29, by wenzelm
modernized specifications;
2012-08-29, by wenzelm
tuned signature;
2012-08-29, by wenzelm
renamed Position.str_of to Position.here;
2012-08-29, by wenzelm
init components from local clone that is used to produce the test distribition, which itself lacks Admin;
2012-08-29, by wenzelm
discontinued centralistic changelog;
2012-08-28, by wenzelm
discontinued odd copy of eps logos (cf. 8fc3828fdc8a);
2012-08-28, by wenzelm
prefer cp over mv, to reduce assumptions about file-system boundaries and GNU vs. non-GNU tools;
2012-08-28, by wenzelm
removed odd left-over file;
2012-08-28, by wenzelm
update on "isabelle build" and "isabelle build_doc";
2012-08-28, by wenzelm
renamed doc-src to src/Doc;
2012-08-28, by wenzelm
do not hardwire document output options -- to be provided by the user;
2012-08-28, by wenzelm
more permanent update of keywords (cf. 3517d6f50b12);
2012-08-28, by wenzelm
merged
2012-08-28, by wenzelm
updated keywords
2012-08-28, by blanchet
fixed import paths in examples
2012-08-28, by blanchet
fixed import paths
2012-08-28, by blanchet
tuning
2012-08-28, by blanchet
updated NEWS and CONTRIBUTORS
2012-08-28, by blanchet
documentation cleanup
2012-08-28, by blanchet
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
2012-08-28, by blanchet
Typo fixed.
2012-08-28, by webertj
updated .hgignore to reflect to (almost) clean result of build_doc;
2012-08-28, by wenzelm
more formal build_doc tool (Admin only);
2012-08-28, by wenzelm
prepare document more uniformly;
2012-08-28, by wenzelm
prefer \input which actually checks file existence;
2012-08-28, by wenzelm
tuned;
2012-08-28, by wenzelm
prefer (old) isa-index as provided here, to get exactly the same index layout as in Isabelle2012;
2012-08-28, by wenzelm
removed old stuff;
2012-08-28, by wenzelm
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
2012-08-28, by wenzelm
removed old stuff;
2012-08-28, by wenzelm
removed historic manual;
2012-08-28, by wenzelm
more standard document preparation within session context;
2012-08-28, by wenzelm
more standard document preparation within session context;
2012-08-28, by wenzelm
updated IsarRef/document/style.sty;
2012-08-28, by wenzelm
missing file;
2012-08-28, by wenzelm
removed junk;
2012-08-28, by wenzelm
more standard document preparation within session context;
2012-08-28, by wenzelm
removed outdated IsarRef/Thy/HOLCF_Specific.thy -- make IsarRef depend on HOL only;
2012-08-28, by wenzelm
prefer doc-src/pdfsetup.sty;
2012-08-28, by wenzelm
more official way to set margin;
2012-08-27, by wenzelm
avoid clash with generated Adaptation.tex on case-insensible file-systems;
2012-08-27, by wenzelm
missing file;
2012-08-27, by wenzelm
deactivate updated doc-src sessions, to make Admin/build doc and makedist work for now;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more portable perl invocation;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
more standard document preparation within session context;
2012-08-27, by wenzelm
clarified "isabelle logo";
2012-08-27, by wenzelm
clarified document directories: browser_info as backdrop vs. optional output directory in the foreground;
2012-08-27, by wenzelm
less ambitious test -- terminate more quickly;
2012-08-27, by wenzelm
tuned;
2012-08-27, by wenzelm
actual use of (sos remote_csdp) via ISABELLE_FULL_TEST;
2012-08-19, by wenzelm
test with many add-ons;
2012-08-27, by wenzelm
updated Theory.begin_theory;
2012-08-26, by wenzelm
entity markup for theory Pure, to enable hyperlinks etc.;
2012-08-26, by wenzelm
more accurate defining position of theory;
2012-08-26, by wenzelm
theory def/ref position reports, which enable hyperlinks etc.;
2012-08-26, by wenzelm
fixed theory dependency
2012-08-26, by nipkow
more convenient switching of buffers;
2012-08-24, by wenzelm
report source path and let front-end resolve implicit master location (e.g. URL);
2012-08-24, by wenzelm
prefer jEdit file name representation (potentially via VFS);
2012-08-24, by wenzelm
more precise counting of line/column;
2012-08-24, by wenzelm
support for direct hyperlinks, without the Hyperlinks plugin;
2012-08-24, by wenzelm
tuned signature;
2012-08-24, by wenzelm
some markup for inlined files;
2012-08-24, by wenzelm
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-08-24, by wenzelm
updated READMEs -- most Mac OS X problems are gone thanks to jdk-7u6;
2012-08-24, by wenzelm
clarified syntax boundary cases and errors;
2012-08-24, by wenzelm
simplified JVM startup, based on stronger assumptions about the Java version provided as Isabelle component;
2012-08-23, by wenzelm
eliminated obsolete byte_reader -- theory headers + body files are parsed in full;
2012-08-23, by wenzelm
more direct File.read_bytes -- avoid cumulative copying of StringBuilder;
2012-08-23, by wenzelm
improved errors of parser combinators;
2012-08-23, by wenzelm
tuned messages: end-of-input rarely means physical end-of-file from the past;
2012-08-23, by wenzelm
merged
2012-08-23, by wenzelm
remove Hoare dependency from Fold.thy
2012-08-23, by Gerwin Klein
added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
2012-08-23, by wenzelm
turned 'boogie_open' into thy_load command, without any declarations of 'uses';
2012-08-23, by wenzelm
tuned signature;
2012-08-23, by wenzelm
clarified type Token.file;
2012-08-23, by wenzelm
expand all files uniformly;
2012-08-23, by wenzelm
added build option -l (list files);
2012-08-23, by wenzelm
prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);
2012-08-23, by wenzelm
more basic file dependencies -- no load command here;
2012-08-23, by wenzelm
tuned signature (again, cf. ff9cd47be39b);
2012-08-23, by wenzelm
updated Thy_Load.check_thy;
2012-08-23, by wenzelm
simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
2012-08-23, by wenzelm
tuned signature;
2012-08-23, by wenzelm
simplified Thy_Load.provide: do not store full path;
2012-08-23, by wenzelm
prefer ML_file over old uses;
2012-08-22, by wenzelm
merged
2012-08-22, by wenzelm
abstracted lemmas
2012-08-21, by nipkow
prefer ML_file over old uses;
2012-08-22, by wenzelm
prefer ML_file over old uses;
2012-08-22, by wenzelm
'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';
2012-08-22, by wenzelm
add keywords of this node as well (e.g. relevant for Pure.thy);
2012-08-22, by wenzelm
tuned;
2012-08-22, by wenzelm
tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;
2012-08-22, by wenzelm
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
2012-08-22, by wenzelm
find files via load commands within theory text;
2012-08-22, by wenzelm
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
2012-08-22, by wenzelm
pass syntax through check_thy;
2012-08-22, by wenzelm
use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader;
2012-08-22, by wenzelm
clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;
2012-08-22, by wenzelm
tuned;
2012-08-22, by wenzelm
clarified bootstrapping of Pure;
2012-08-22, by wenzelm
tuned errors;
2012-08-22, by wenzelm
prefer File.full_path in accordance to check_file;
2012-08-21, by wenzelm
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
2012-08-21, by wenzelm
updated Thy_Load.check_thy;
2012-08-21, by wenzelm
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
2012-08-21, by wenzelm
more direct cumulation of (sparse) keywords;
2012-08-21, by wenzelm
some support for thy_load_commands;
2012-08-21, by wenzelm
tuned signature;
2012-08-21, by wenzelm
clarified initialization of Thy_Load, Thy_Info, Session;
2012-08-21, by wenzelm
tuned;
2012-08-21, by wenzelm
more robust cleaning of "% tag" and "-- cmt";
2012-08-20, by wenzelm
some support for inlining file content into outer syntax token language;
2012-08-20, by wenzelm
tuned comment;
2012-08-20, by wenzelm
tuned;
2012-08-20, by wenzelm
added keyword kind "thy_load" (with optional list of file extensions);
2012-08-20, by wenzelm
updated generated files;
2012-08-20, by wenzelm
more strict syntax, according to manual;
2012-08-20, by wenzelm
abstracted lemma
2012-08-20, by nipkow
retain unknown options within preferences;
2012-08-19, by wenzelm
more comprehensible platform family name;
2012-08-19, by wenzelm
tuned message;
2012-08-19, by wenzelm
fewer components, more roots;
2012-08-19, by wenzelm
actually remove makeall (cf. 292b97e17fb7);
2012-08-19, by wenzelm
tuned;
2012-08-17, by wenzelm
Backed out changeset ec82c33c75f8;
2012-08-17, by wenzelm
Typo fixed.
2012-08-17, by webertj
merged
2012-08-17, by wenzelm
merged
2012-08-17, by nipkow
fixed lemmas
2012-08-17, by nipkow
abstracted lemmas
2012-08-16, by nipkow
updated to new init_components, hoping that mira can digest that;
2012-08-17, by wenzelm
some explanations on component categories;
2012-08-17, by wenzelm
specific cygwin components;
2012-08-17, by wenzelm
obsolete;
2012-08-17, by wenzelm
some explanations on isabelle components;
2012-08-17, by wenzelm
some grouping of components;
2012-08-17, by wenzelm
renamed components to components_old, to make room for some directory of the same name;
2012-08-17, by wenzelm
minor robustification;
2012-08-17, by wenzelm
added "isabelle components" tool;
2012-08-17, by wenzelm
tuned;
2012-08-17, by wenzelm
direct support for component forests via init_components;
2012-08-17, by wenzelm
allow to provide external ISABELLE_IDENTIFIER for repository clone -- potentially relevant for isatest and mira;
2012-08-17, by wenzelm
tuned;
2012-08-17, by wenzelm
tuned;
2012-08-17, by wenzelm
updated component repository;
2012-08-17, by wenzelm
updates on 32 bit vs. 64 bit platforms;
2012-08-17, by wenzelm
updated to jedit_build-20120813, pointing to another contrib directory as a change;
2012-08-17, by wenzelm
merged
2012-08-16, by wenzelm
tuned proofs;
2012-08-16, by wenzelm
look in current directory first before looking up includes in the TPTP directory, as required by Geoff
2012-08-16, by blanchet
prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala
2012-08-16, by haftmann
more robust multi-platform support;
2012-08-16, by wenzelm
updated to jdk-7u6 and jedit_build-20120813 -- NB: plain Isabelle/Scala still happens to work with jdk-6;
2012-08-16, by wenzelm
support for jdk-7u6 component;
2012-08-16, by wenzelm
Clarification: free variables allowed in interpreted locale instances.
2012-08-15, by ballarin
merged
2012-08-15, by nipkow
fixed proof
2012-08-15, by nipkow
abstracted lemmas
2012-08-15, by nipkow
Backed out changeset 6cf7a9d8bbaf
2012-08-15, by nipkow
abstracted lemmas
2012-08-15, by nipkow
merged
2012-08-15, by webertj
Turned into Admin tool download_components.
2012-08-15, by webertj
tuned;
2012-08-15, by wenzelm
tuned;
2012-08-15, by wenzelm
some updates of "Presenting theories", using mkroot/build instead of former mkdir/make/usedir (which are still present in "Misc");
2012-08-15, by wenzelm
tuned;
2012-08-15, by wenzelm
fixed handling of "int" in the wake of its port to the quotient package
2012-08-15, by blanchet
removed dead code
2012-08-15, by blanchet
merged
2012-08-15, by webertj
Added various options, notably -c to download components listed in Admin/components. Also, curl instead of wget.
2012-08-15, by webertj
ignore some administrative files on newer Mercurial versions as well;
2012-08-14, by wenzelm
some support for persistent user preferences;
2012-08-14, by wenzelm
merged
2012-08-14, by wenzelm
explicit document_output directory, without implicit purge of default in ISABELLE_BROWSER_INFO;
2012-08-14, by wenzelm
more direct interpretation of document_variants for build (unchanged for usedir);
2012-08-14, by wenzelm
tone down "z3_tptp", now that Z3 (starting with 4.1) no longer supports TPTP TFF0
2012-08-14, by blanchet
fixed then-else confusion
2012-08-14, by blanchet
tweak Vampire setup in the light of new evaluation
2012-08-14, by blanchet
improved set of reconstructor methods
2012-08-14, by blanchet
warn users about unused "using" facts
2012-08-14, by blanchet
be less aggressive at kicking out chained facts
2012-08-14, by blanchet
recognize bus errors as crash
2012-08-14, by blanchet
consider removing chained facts last, so that they're more likely to be kept
2012-08-14, by blanchet
clarified format of etc/options: only declarations, not re-definitions;
2012-08-14, by wenzelm
check_errors for cumulative session content;
2012-08-14, by wenzelm
even more defensive path expansion (see also 8d381fdef898);
2012-08-14, by wenzelm
support for 'typ' with explicit sort constraint;
2012-08-14, by wenzelm
added jedit option -d;
2012-08-14, by wenzelm
always retain doc-src (as regular component);
2012-08-14, by wenzelm
merged
2012-08-13, by wenzelm
Calling isabelle with proper (relative) path, no longer relying on $PATH.
2012-08-13, by webertj
fewer workarounds for MacOS to increase chances that COMMAND ("META") key works with Java 1.7 from Oracle;
2012-08-13, by wenzelm
updated to jedit-4.5.2 (still unchanged);
2012-08-13, by wenzelm
restored ISABELLE_OUTPUT etc -- still relevant at least for mira.py itself
2012-08-12, by krauss
tuned;
2012-08-12, by wenzelm
fixed mira.py (cf. fd50596bf78b)
2012-08-12, by krauss
more direct embedding of abstract thm values into the ML environment -- avoidance of repeated ML_Thms.the_thm(s) considerably reduces compilation time for Poly/ML 5.4.x;
2012-08-12, by wenzelm
more static antiquotations;
2012-08-12, by wenzelm
always show some timing information, to reduce the need for explicit -v;
2012-08-12, by wenzelm
some information for central Isabelle repository configuration;
2012-08-12, by wenzelm
reduced settings patching
2012-08-12, by krauss
removed obsolete configuration AFP_images
2012-08-12, by krauss
faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-08-11, by wenzelm
simplified symbol matching;
2012-08-11, by wenzelm
further clarification of malformed symbols;
2012-08-11, by wenzelm
more liberal scanning of potentially malformed symbols;
2012-08-11, by wenzelm
vacuous execution after first malformed command;
2012-08-11, by wenzelm
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
2012-08-11, by wenzelm
tuned markup;
2012-08-11, by wenzelm
tuned message;
2012-08-11, by wenzelm
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
2012-08-11, by wenzelm
reports with body text, not just markup;
2012-08-11, by wenzelm
fixed "double rev" bug that arose in situations where a % comment arose on the last line of a file without \n at the end
2012-08-11, by blanchet
special code with lists no longer necessary, use sets
2012-08-11, by nipkow
proper error prefixes;
2012-08-10, by wenzelm
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
2012-08-10, by wenzelm
tuned message;
2012-08-10, by wenzelm
clarified Linear_Set.next/prev: check definedness;
2012-08-10, by wenzelm
merged
2012-08-10, by nipkow
Improved complete lattice formalisation - no more index set.
2012-08-10, by nipkow
merged
2012-08-10, by wenzelm
tuned proofs;
2012-08-10, by wenzelm
sneak message into "bad" markup as property -- to be displayed after YXML parsing;
2012-08-10, by wenzelm
apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
2012-08-10, by wenzelm
clarified undefined, unparsed, unfinished command spans;
2012-08-10, by wenzelm
tuned;
2012-08-10, by wenzelm
discontinued mostly unused markup for command spans;
2012-08-10, by wenzelm
more visible markup of malformed input as "bad";
2012-08-10, by wenzelm
tuned proofs
2012-08-10, by blanchet
some attempts to keep malformed syntax errors focussed, without too much red spilled onto the document view;
2012-08-09, by wenzelm
refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
2012-08-09, by wenzelm
tuned signature;
2012-08-09, by wenzelm
more direct Linear_Set.reverse, swapping orientation of the graph;
2012-08-09, by wenzelm
tuned signature;
2012-08-09, by wenzelm
tuned;
2012-08-09, by wenzelm
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
2012-08-09, by wenzelm
explicit FIXME;
2012-08-09, by wenzelm
tuned signature;
2012-08-09, by wenzelm
corrected header
2012-08-08, by haftmann
refined isabelle mkroot;
2012-08-08, by wenzelm
simplified session specifications: names are taken verbatim and current directory is default;
2012-08-08, by wenzelm
added build option -D: include session directory and select its sessions;
2012-08-08, by wenzelm
discontinued obsolete "isabelle makeall";
2012-08-08, by wenzelm
even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
2012-07-27, by wenzelm
back to implicit commit via isabelle-process -- save image only once (cf. 181b91e1d1c1);
2012-08-08, by wenzelm
proper axiomatization of "mem" -- do not leave it formally unspecified;
2012-08-08, by wenzelm
simplified Pure bootstrap -- separate pure_setup.ML was required for Alice/ML at some point;
2012-08-08, by wenzelm
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
2012-08-08, by wenzelm
obsolete;
2012-08-08, by wenzelm
eliminated obsolete ISABELLE_USEDIR_OPTIONS;
2012-08-08, by wenzelm
updated ML settings;
2012-08-08, by wenzelm
add legacy target for HOL-Probability, needed by AFP/Markov_Models
2012-08-08, by hoelzl
proper isabelle update_keywords tool;
2012-08-08, by wenzelm
configure Admin as component, with its own lib/Tools;
2012-08-08, by wenzelm
SOMEthing went utterly wrong in 5b51ccdc8623;
2012-08-08, by wenzelm
more legacy targets;
2012-08-08, by wenzelm
discontinued obsolete IsaMakefile and ROOT.ML files from the Isabelle distribution;
2012-08-07, by wenzelm
tuned;
2012-08-07, by wenzelm
proper quoting
2012-08-07, by blanchet
merged
2012-08-07, by wenzelm
more structural parsing for minor modes;
2012-08-07, by wenzelm
clarified Sidekick configuration, including minor modes;
2012-08-07, by wenzelm
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
2012-08-07, by blanchet
specify full path to clausifier
2012-08-07, by blanchet
documentation
2012-08-07, by blanchet
more token markers, based on actual outer syntax;
2012-08-07, by wenzelm
simplified process startup phases: INIT suffices for is_ready;
2012-08-07, by wenzelm
need to expand path in order to resolve imports like "~~/src/Tools/Code_Generator";
2012-08-07, by wenzelm
prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
2012-08-07, by wenzelm
prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
2012-08-07, by wenzelm
permissive outer syntax wrt. symbol recoding;
2012-08-07, by wenzelm
simplified Document.Node.Header -- internalized errors;
2012-08-07, by wenzelm
tuned signature;
2012-08-07, by wenzelm
tuned signature -- slightly more abstract text representation of prover process;
2012-08-07, by wenzelm
tuned signature -- make Pretty less dependent on Symbol;
2012-08-07, by wenzelm
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
2012-08-07, by boehmes
increase defensive timeout that should typically not kick in thanks to solid time limits in Sledgehammer (otherwise, Mirabelle-based evaluations might be distorted)
2012-08-07, by boehmes
documentation
2012-08-06, by blanchet
added iProver(-Eq) local
2012-08-06, by blanchet
optimized saving
2012-08-06, by blanchet
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
2012-08-06, by wenzelm
merged
2012-08-06, by wenzelm
switching from Emacs.app to Aquamacs.app
2012-08-06, by paulson
switching from Emacs.app to Aquamacs.app
2012-08-06, by paulson
modify group_cancel simprocs so that they can cancel multiple terms at once
2012-08-06, by huffman
"isabelle options" prints Isabelle system options;
2012-08-06, by wenzelm
removed leftover from 89cc3dfb383b, hoping that mira digests it;
2012-08-06, by wenzelm
discontinued presumably obsolete attempts at doc-src testing (cf. 3b02b0ef8d48, 89cc3dfb383b);
2012-08-06, by wenzelm
more precise imitation of old ROOT.ML files;
2012-08-06, by wenzelm
fixed mira.py (cf. fe611991427a)
2012-08-05, by krauss
corrected session name
2012-08-05, by krauss
removed obsolete mira configurations -- covered by AFP_images
2012-08-05, by krauss
modernized mira configurations, making use of isabelle build
2012-08-05, by krauss
removed mira configurations related to old importer
2012-08-05, by krauss
re-introduced ROOTS catalog files (cf. 47330b712f8f) which help to organize AFP or make -d options persistent;
2012-08-05, by wenzelm
more on isabelle mkroot;
2012-08-05, by wenzelm
added mkroot: prepare session root directory;
2012-08-05, by wenzelm
prefer general Command_Line.tool wrapper (cf. Scala version);
2012-08-05, by wenzelm
simplified Session_Tree;
2012-08-05, by wenzelm
some timeouts, which modify the build order;
2012-08-04, by wenzelm
queue ordering by descending outdegree and timeout;
2012-08-04, by wenzelm
tuned import;
2012-08-04, by wenzelm
clarified Session_Tree (with proper integrity check) vs. Queue (with provision for alternative ordering);
2012-08-04, by wenzelm
clarified Session_Entry vs. Session_Info with related parsing operations;
2012-08-04, by wenzelm
simplified class Job;
2012-08-04, by wenzelm
let with_timing report overall number of threads;
2012-08-04, by wenzelm
further robustification of interrupts during build;
2012-08-04, by wenzelm
refined outer syntax;
2012-08-04, by wenzelm
prefer calligrapic \<RR> \<II> over \<Re> \<Im> for "screen" display (NB: official unicode defines only one version of these glyphs, unlike TeX);
2012-08-03, by wenzelm
remember ATP flops to avoid repeating them too quickly
2012-08-03, by blanchet
remember which MaSh proofs were found using ATPs
2012-08-03, by blanchet
rule out same "technical" theories for MePo as for MaSh
2012-08-03, by blanchet
don't generate queries for empty dependencies
2012-08-03, by blanchet
crank up max number of dependencies
2012-08-03, by blanchet
never use MaSh in Metis examples, to avoid one dimension of nondeterminism
2012-08-03, by blanchet
merged
2012-08-03, by wenzelm
more informative process exit code;
2012-08-03, by wenzelm
timeout for session build job;
2012-08-03, by wenzelm
static outer syntax based on session specifications;
2012-08-03, by wenzelm
declare trE and tr_induct as default cases and induct rules for type tr
2012-08-03, by huffman
reject path variable nesting explicitly;
2012-08-03, by wenzelm
simplified custom document/build script, instead of old-style document/IsaMakefile;
2012-08-03, by wenzelm
cleaner temporary file cleanup for MaSh, based on tried-and-trusted code
2012-08-03, by blanchet
merged
2012-08-02, by wenzelm
don't tag negatively naked variables
2012-08-02, by blanchet
support older versions of Vampire
2012-08-02, by blanchet
document E-MaLeS
2012-08-02, by blanchet
added E-MaLeS to list of provers for testing
2012-08-02, by blanchet
discontinued unused etc/sessions catalog;
2012-08-02, by wenzelm
allow session specifications in arbitrary order;
2012-08-02, by wenzelm
tuned;
2012-08-02, by wenzelm
report commands as formal entities, with def/ref positions;
2012-08-02, by wenzelm
more official command specifications, including source position;
2012-08-02, by wenzelm
more antiquotations;
2012-08-02, by wenzelm
declare keywords only once;
2012-08-02, by wenzelm
more antiquotations;
2012-08-02, by wenzelm
more antiquotations;
2012-08-02, by wenzelm
more standard bootstrapping of Pure outer syntax;
2012-08-01, by wenzelm
fixed document;
2012-08-01, by wenzelm
store parent heap stamp as well -- needs to be propagated through the build hierarchy;
2012-08-01, by wenzelm
more standard bootstrapping of Pure.thy;
2012-08-01, by wenzelm
more precise guide for bibtex/makeindex -- dummy files should be sufficient;
2012-08-01, by wenzelm
added offline test for skip_proofs;
2012-08-01, by wenzelm
clarified ISABELLE_FULL_TEST;
2012-08-01, by wenzelm
explicit option skip_proofs;
2012-08-01, by wenzelm
recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);
2012-08-01, by wenzelm
removed junk;
2012-08-01, by wenzelm
no longer force STIX fonts onto the user -- NB: STIXv1.0.0 is outdated and Mac OS 10.7 ships its own copy of STIX already;
2012-08-01, by wenzelm
more prominent file name;
2012-08-01, by wenzelm
updated isatest settings for isabelle build;
2012-07-31, by wenzelm
more portable hex_nibble: avoid disagreement of Poly/ML and SML/NJ on StringCvt.HEX;
2012-07-31, by wenzelm
merged
2012-07-31, by wenzelm
print full path;
2012-07-31, by wenzelm
Remove Lift_RBT.thy, it's in HOL/Library/RBT.thy now
2012-07-31, by kuncar
add testing file for RBT_Set
2012-07-31, by kuncar
implementation of sets by RBT trees for the code generator
2012-07-31, by kuncar
use lifting/transfer formalization of RBT from Lift_RBT
2012-07-31, by kuncar
a couple of additions to RBT formalization to allow us to implement RBT_Set
2012-07-31, by kuncar
more relation operations expressed by Finite_Set.fold
2012-07-31, by kuncar
more set operations expressed by Finite_Set.fold
2012-07-31, by kuncar
moved another larger quickcheck example to Quickcheck_Benchmark
2012-07-26, by bulwahn
HOL-Probability appears to work with smlnj;
2012-07-31, by wenzelm
document variant NAME may use different LaTeX entry point document/root_NAME.tex if that file exists;
2012-07-31, by wenzelm
made SML/NJ happy;
2012-07-31, by wenzelm
renamed session TLA to HOL-TLA to avoid clash with AFP;
2012-07-31, by wenzelm
clarified directory content operations (similar to ML version);
2012-07-30, by wenzelm
regenerate ToyList2/ToyList.thy during raw make *after* session build, to ensure that it is updated sporadically (NB: isabelle build does not support generated sources);
2012-07-30, by wenzelm
multi-threaded HOL-Tutorial with explicit indication of local options;
2012-07-30, by wenzelm
removed obsolete IsaMakefile + ROOT.ML setup -- doc-src is managed via isabelle build;
2012-07-30, by wenzelm
removed some old material (inactive since 2002/2003);
2012-07-30, by wenzelm
updated isatest to isabelle build, which also includes doc-src sessions;
2012-07-30, by wenzelm
obsolete;
2012-07-30, by wenzelm
makedist -D retains doc-src component with its "doc" sessions (relevant for testing);
2012-07-30, by wenzelm
allow negative int values as well, according to real = int | float;
2012-07-30, by wenzelm
misc tuning;
2012-07-30, by wenzelm
discontinued unused isabelle jedit debugger;
2012-07-30, by wenzelm
more uniform usage of "isabelle tool";
2012-07-30, by wenzelm
less verbosity;
2012-07-30, by wenzelm
proper treatment of eof wrt. proper_input -- allow input of spaces/comments only;
2012-07-30, by wenzelm
tuned signature;
2012-07-30, by wenzelm
updated ROOT according to 3defa60a7ae3;
2012-07-30, by wenzelm
merged
2012-07-30, by wenzelm
re-activating Quickcheck_Narrowing_Examples in Quickcheck_Examples
2012-07-30, by bulwahn
added build option -c;
2012-07-30, by wenzelm
removed build option -f (cf. a125b8040ada), due to slightly inconvenient behaviour on ancestors;
2012-07-30, by wenzelm
script for downloading components from central store
2012-07-29, by haftmann
added build option -f;
2012-07-29, by wenzelm
corrected slip
2012-07-28, by haftmann
discontinued $ISABELLE_HOME/build (cf. 500c6eb6c6dc);
2012-07-28, by wenzelm
separate session HOL-Mirabelle-ex -- cannot run isolated shell scripts within build tool;
2012-07-28, by wenzelm
added Quickcheck_Benchmark (cf. 1959baa22632);
2012-07-28, by wenzelm
no apparent need for single-threaded execution;
2012-07-28, by wenzelm
discontinued obsolete Isabelle/build script;
2012-07-28, by wenzelm
announce advanced support for Isabelle sessions and build management;
2012-07-28, by wenzelm
some introduction on sessions;
2012-07-28, by wenzelm
tuned messages;
2012-07-28, by wenzelm
tuned;
2012-07-28, by wenzelm
added generated file;
2012-07-28, by wenzelm
some description of main build options;
2012-07-28, by wenzelm
more on "Session ROOT specifications";
2012-07-28, by wenzelm
some description of isabelle build;
2012-07-28, by wenzelm
tuned;
2012-07-28, by wenzelm
isabelle browser is another user interface;
2012-07-28, by wenzelm
renamed isabelle-root minor mode;
2012-07-28, by wenzelm
discontinued special treatment of Proof General;
2012-07-28, by wenzelm
top-down order of user interfaces;
2012-07-28, by wenzelm
misc tuning;
2012-07-28, by wenzelm
move exception handlers outside of let block
2012-07-28, by huffman
tuned message;
2012-07-27, by wenzelm
merged
2012-07-27, by wenzelm
evaluation: allow multiple code modules
2012-07-27, by haftmann
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
2012-07-27, by wenzelm
merged
2012-07-27, by wenzelm
restored narrowing quickcheck after 6efff142bb54
2012-07-27, by haftmann
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
2012-07-27, by wenzelm
unvarify thm statement stemming from old-style definition, to avoid schematic type variables in subsequent goal;
2012-07-27, by wenzelm
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
2012-07-27, by wenzelm
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
2012-07-27, by huffman
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
2012-07-27, by huffman
give Nat_Arith simprocs proper name bindings by using simproc_setup
2012-07-27, by huffman
tweaks in preparation for type encoding evaluation
2012-07-27, by blanchet
merged
2012-07-27, by wenzelm
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
2012-07-27, by huffman
nicer Nitpick subscript output in jEdit
2012-07-27, by blanchet
no_check for @{setting} antiquotations -- empty values are treated as undefined on Cygwin;
2012-07-27, by wenzelm
proper shell variable;
2012-07-27, by wenzelm
actually check return code;
2012-07-27, by wenzelm
include doc-src as component, and thus its sessions defined in ROOT;
2012-07-27, by wenzelm
tuned signature;
2012-07-27, by wenzelm
delete other log file;
2012-07-27, by wenzelm
simplified Path vs. JVM File operations;
2012-07-27, by wenzelm
tuned;
2012-07-27, by wenzelm
tuned messages;
2012-07-27, by wenzelm
fewer options;
2012-07-27, by wenzelm
tuned signature;
2012-07-27, by wenzelm
prefer explicit datatype Present.dump_mode;
2012-07-27, by wenzelm
simplified Session.name;
2012-07-27, by wenzelm
more precise imitation of usedir wrt. Session.name (cf. 45137257399a);
2012-07-27, by wenzelm
update docs
2012-07-27, by blanchet
extract Z3 unsat cores (for "z3_tptp")
2012-07-27, by blanchet
bring implementation of traditional encoding in line with paper
2012-07-27, by blanchet
further refinement of current/all_current status, which needs to be propagated through the hierarchy (see also Thy_Info.require_thys);
2012-07-26, by wenzelm
merged
2012-07-26, by wenzelm
[1] goes after any attributes
2012-07-26, by blanchet
Z3 prints so many warnings that the very informative abnormal termination exception hardly ever gets raised -- better be more aggressive here
2012-07-26, by blanchet
detect unknown options again
2012-07-26, by blanchet
Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
2012-07-26, by blanchet
don't export technical theorems for MaSh
2012-07-26, by blanchet
repaired accessibility chains generated by MaSh exporter + tuned one function out
2012-07-26, by blanchet
generate fact name in queries again + use ATP dependencies when possible
2012-07-26, by blanchet
proper all_current, which regards parent status as well;
2012-07-26, by wenzelm
more build options;
2012-07-26, by wenzelm
added session HOL-Tutorial;
2012-07-26, by wenzelm
recovered chapter on Presenting Theories;
2012-07-26, by wenzelm
avoid clash of Misc/pairs.thy and Types/Pairs.thy on case-insensible file-system;
2012-07-26, by wenzelm
proper input;
2012-07-26, by wenzelm
recovered latex job;
2012-07-26, by wenzelm
adhoc reordering to prevent implicit side-effects of some theories in Types, Rules, Sets;
2012-07-26, by wenzelm
more build options;
2012-07-26, by wenzelm
simplified Tutorial sessions;
2012-07-26, by wenzelm
proper arguments for old usedir;
2012-07-26, by wenzelm
more precise imports;
2012-07-26, by wenzelm
refined "document_dump_mode": "all", "tex+sty", "tex";
2012-07-26, by wenzelm
allow spaces in file names;
2012-07-26, by wenzelm
more files for session Pure;
2012-07-26, by wenzelm
discontinued slightly odd "browser_info_remote" -- it could point to a completely different version of the Isabelle library;
2012-07-26, by wenzelm
tuned;
2012-07-26, by wenzelm
remove old output heaps, to ensure that result is valid wrt. check_stamps;
2012-07-26, by wenzelm
proper imports;
2012-07-26, by wenzelm
support session groups;
2012-07-26, by wenzelm
discontinued slightly odd session order, which did not quite work out;
2012-07-26, by wenzelm
tuned signature;
2012-07-26, by wenzelm
avoid clash of Advanced/simp.thy vs. Misc/simp.thy;
2012-07-25, by wenzelm
tuned signature;
2012-07-25, by wenzelm
actually check source vs. target stamps, based on information from log files;
2012-07-25, by wenzelm
tuned;
2012-07-25, by wenzelm
session specifications for doc-src, excluding TutorialI for now;
2012-07-25, by wenzelm
updated generated files;
2012-07-25, by wenzelm
clarified no_document situation;
2012-07-25, by wenzelm
no hardwired default for Proof General component -- its users can use init_component separately;
2012-07-25, by wenzelm
rail no longer exists;
2012-07-25, by wenzelm
some updates on "Building a repository version of Isabelle";
2012-07-25, by wenzelm
added condition = ISABELLE_POLYML according to no-smlnj targets in IsaMakefile;
2012-07-25, by wenzelm
more standard session setup for WWW_Find;
2012-07-25, by wenzelm
read/write dependency information;
2012-07-24, by wenzelm
more files;
2012-07-24, by wenzelm
more build options;
2012-07-24, by wenzelm
merged
2012-07-24, by wenzelm
moving a first Quickcheck example with many computations into a separate session Quickcheck_Benchmark
2012-07-24, by bulwahn
moving Quickcheck_Examples back to test to run a minimal test even with the mira testing infrastructure
2012-07-24, by bulwahn
reactivated HOL-NSA-Examples;
2012-07-24, by wenzelm
tuned order;
2012-07-24, by wenzelm
more build options;
2012-07-24, by wenzelm
tuned error;
2012-07-24, by wenzelm
more explicit checks during parsing;
2012-07-24, by wenzelm
more explicit document = false to reduce warnings;
2012-07-24, by wenzelm
pass parent_base_name, which is required for Session.init sanity check;
2012-07-24, by wenzelm
more session entries;
2012-07-24, by wenzelm
modernized imports;
2012-07-24, by wenzelm
more general notion of user ERROR (cf. 44f56fe01528);
2012-07-24, by wenzelm
tuned messages;
2012-07-24, by wenzelm
tuned message;
2012-07-24, by wenzelm
human-readable I/O error;
2012-07-24, by wenzelm
more session ROOT files;
2012-07-24, by wenzelm
tuned messages (cf. isabelle makeall);
2012-07-24, by wenzelm
tuned message;
2012-07-24, by wenzelm
actually negate "document" (cf. 7483aa690b4f);
2012-07-24, by wenzelm
clarified no_build vs. verbose;
2012-07-24, by wenzelm
clarified "document" again, eliminated redundant "no_document";
2012-07-24, by wenzelm
clarified build -n (no build);
2012-07-24, by wenzelm
added "document_dump_only" (cf. negated usedir -C);
2012-07-24, by wenzelm
more precise propagation of options: build, session, theories;
2012-07-24, by wenzelm
further imitation of ISABELLE_USEDIR_OPTIONS via options;
2012-07-24, by wenzelm
observe "condition";
2012-07-24, by wenzelm
observe "quick_and_dirty";
2012-07-24, by wenzelm
added "browser_info_remote" (cf. usedir -P);
2012-07-24, by wenzelm
clarified "this_name" vs. former "reset" feature -- imitate the latter by loading other session sources directly;
2012-07-24, by wenzelm
timing for whole session;
2012-07-24, by wenzelm
tuned options;
2012-07-24, by wenzelm
timing is command line options, not system option;
2012-07-24, by wenzelm
clarified document options;
2012-07-24, by wenzelm
pass build options to ML;
2012-07-24, by wenzelm
added ML version of stand-alone options, with XML.encode/decode operations (unidirectional from Scala to ML);
2012-07-23, by wenzelm
provide explicit ISABELLE_PLATFORM32 as well;
2012-07-23, by wenzelm
merged
2012-07-23, by berghofe
set_vcs now derives prefix from fully qualified procedure / function name
2012-07-23, by berghofe
try droppable application using Platypus functionality -- in contrast to earlier AppHack (cf. 9343d4b7c5bf);
2012-07-23, by wenzelm
updated to Platypus 4.7;
2012-07-23, by wenzelm
merged
2012-07-23, by wenzelm
tuned;
2012-07-23, by wenzelm
clarified init_component: always liberal;
2012-07-23, by wenzelm
added system build mode: produce output in ISABELLE_HOME;
2012-07-23, by wenzelm
removed redundant check (cf. a8ed41b6280b);
2012-07-23, by wenzelm
pass ISABELLE_BROWSER_INFO as explicit argument;
2012-07-23, by wenzelm
removed some old/unused stuff;
2012-07-23, by wenzelm
updated smlnj settings;
2012-07-23, by wenzelm
cap the number of facts returned by MaSh
2012-07-23, by blanchet
remove MaSh junk associated with size functions
2012-07-23, by blanchet
identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway
2012-07-23, by blanchet
removed MaSh junk arising from primrec definitions
2012-07-23, by blanchet
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
2012-07-23, by blanchet
tuning
2012-07-23, by blanchet
faster "save" operation
2012-07-23, by blanchet
include unknown local facts in MaSh
2012-07-23, by blanchet
ensure all calls to "mash" program are synchronous
2012-07-23, by blanchet
don't relearn old facts in Isar mode
2012-07-23, by blanchet
took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
2012-07-23, by blanchet
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
2012-07-23, by haftmann
more correct import
2012-07-23, by haftmann
merged
2012-07-22, by wenzelm
NEWS
2012-07-22, by haftmann
library theories for debugging and parallel computing using code generation towards Isabelle/ML
2012-07-22, by haftmann
also consider current working directory (cf. 3a5a5a992519)
2012-07-21, by haftmann
parallel scheduling of jobs;
2012-07-22, by wenzelm
tuned;
2012-07-22, by wenzelm
maintain set of source digests, including relevant parts of session entry;
2012-07-22, by wenzelm
determine source dependencies, relatively to preloaded theories;
2012-07-22, by wenzelm
propagate defined options;
2012-07-21, by wenzelm
disallow quotes in path specifications -- extra paranoia;
2012-07-21, by wenzelm
save image for inner nodes only;
2012-07-21, by wenzelm
some actual build function on ML side;
2012-07-21, by wenzelm
tuned -- no dependency on exit function;
2012-07-21, by wenzelm
more ML_System operations;
2012-07-21, by wenzelm
restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs
2012-07-21, by bulwahn
handling partiality in the case where the equality optimisation is applied
2012-07-21, by bulwahn
merged
2012-07-20, by wenzelm
updated File.find_files;
2012-07-20, by wenzelm
more abstract file system operations in Scala, corresponding to ML version;
2012-07-20, by wenzelm
eliminated obsolete session_manager.scala;
2012-07-20, by wenzelm
more explicit java.io.{File => JFile};
2012-07-20, by wenzelm
tune Mesh filter
2012-07-20, by blanchet
faster maximal node computation
2012-07-20, by blanchet
honor suggested MaSh weights
2012-07-20, by blanchet
use CVC3 and Yices by default if they are available and there are enough cores
2012-07-20, by blanchet
relearn ATP proofs
2012-07-20, by blanchet
don't store fresh names in fact graph, since these cannot be the parents of any other facts
2012-07-20, by blanchet
added MaSh to news
2012-07-20, by blanchet
cached ancestor computation
2012-07-20, by blanchet
minimal maxes + tuning
2012-07-20, by blanchet
learn from SMT proofs when they can be minimized by Metis
2012-07-20, by blanchet
clean up interesting constants a bit
2012-07-20, by blanchet
convenience
2012-07-20, by blanchet
name tuning
2012-07-20, by blanchet
learning should honor the fact override and the chained facts
2012-07-20, by blanchet
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
2012-07-20, by blanchet
MaSh docs
2012-07-20, by blanchet
added "learn_from_atp" command to MaSh, for patient users
2012-07-20, by blanchet
get rid of redundant "xxx_INSTALLED" environment variabl
2012-07-20, by blanchet
add versioning to MaSh state + cleanup dead code
2012-07-20, by blanchet
eliminated special handling of init case, now that "mash.py" has been optimized to handle sequences of add gracefully
2012-07-20, by blanchet
more MaSh docs
2012-07-20, by blanchet
mention MaSh in docs
2012-07-20, by blanchet
use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them
2012-07-20, by blanchet
added locality as a MaSh feature
2012-07-20, by blanchet
learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
2012-07-20, by blanchet
learn command in MaSh
2012-07-20, by blanchet
added possibility of running external MaSh commands asynchronously
2012-07-20, by blanchet
renamed ML structures
2012-07-20, by blanchet
renamed ML files
2012-07-20, by blanchet
renamed "iter" fact filter to "MePo" (Meng--Paulson)
2012-07-20, by blanchet
handle local facts smoothly in MaSh
2012-07-20, by blanchet
fixed explosion when computing accessibility
2012-07-20, by blanchet
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
2012-07-20, by blanchet
tuning
2012-07-20, by blanchet
merged
2012-07-20, by wenzelm
further imitation of "usedir" shell script;
2012-07-20, by wenzelm
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
2012-07-20, by huffman
export code relatively to master directory
2012-07-19, by haftmann
require explicit initialization of options;
2012-07-20, by wenzelm
tuned signature;
2012-07-20, by wenzelm
define build_options from command line;
2012-07-20, by wenzelm
some basic Isabelle options;
2012-07-20, by wenzelm
basic jEdit mode for Isabelle options;
2012-07-20, by wenzelm
basic support for stand-alone options with external string representation;
2012-07-20, by wenzelm
minimal build_job;
2012-07-20, by wenzelm
restrict to required sessions;
2012-07-20, by wenzelm
proper commas_quote;
2012-07-20, by wenzelm
tune;
2012-07-20, by wenzelm
simplified script to build Isabelle/ML;
2012-07-20, by wenzelm
added eq_file / copy_file corresponding to File.eq / File.copy in ML;
2012-07-19, by wenzelm
merged
2012-07-19, by wenzelm
removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)
2012-07-19, by haftmann
deactivating quickcheck narrowing examples to find out if this causes the system error on the current isatest
2012-07-19, by bulwahn
support for detached Bash_Job with some control operations;
2012-07-19, by wenzelm
allow catalog entries to be commented-out;
2012-07-19, by wenzelm
support external processes with explicit environment;
2012-07-19, by wenzelm
include COMPONENT/etc/sessions as catalog for more directories, for improved scalability with hundreds of entries (notably AFP);
2012-07-19, by wenzelm
less redundant data structures;
2012-07-19, by wenzelm
clarified topological ordering: preserve order of adjacency via reverse fold;
2012-07-19, by wenzelm
support Session.Queue with ordering and dependencies;
2012-07-19, by wenzelm
clarified signature;
2012-07-19, by wenzelm
more explicit treatment of initial Pure sessions;
2012-07-19, by wenzelm
more general support for Isabelle/Scala command line tools;
2012-07-19, by wenzelm
tuned width;
2012-07-19, by wenzelm
prefer general Properties.Value.Boolean;
2012-07-19, by wenzelm
more SHA1.digest operations;
2012-07-18, by wenzelm
tuned import;
2012-07-18, by wenzelm
tuned source structure;
2012-07-18, by wenzelm
allow explicit specification of additional session directories;
2012-07-18, by wenzelm
more errors;
2012-07-18, by wenzelm
some HOL sessions;
2012-07-18, by wenzelm
cumulate semantic Session_Info, based on syntactic Session_Entry;
2012-07-18, by wenzelm
more tight treatment of reset_name;
2012-07-18, by wenzelm
more informative errors;
2012-07-18, by wenzelm
added parser for Session_Info;
2012-07-18, by wenzelm
repair MaSh exporter
2012-07-18, by blanchet
optimize parent computation in MaSh + remove temporary files
2012-07-18, by blanchet
make the monomorphizer more predictable by making the cutoff independent on the number of facts
2012-07-18, by blanchet
speed up MaSh queries
2012-07-18, by blanchet
use better score function, based on previous evaluation (cf. Deduct 2011 slides)
2012-07-18, by blanchet
attempt at meshing according to more meaningful factors
2012-07-18, by blanchet
don't include hidden facts in relevance filter + tweak MaSh learning
2012-07-18, by blanchet
removed debugging output
2012-07-18, by blanchet
removed expensive HO check in MaSh
2012-07-18, by blanchet
speed up tautology/metaness check
2012-07-18, by blanchet
optimized MaSh output by chunking it
2012-07-18, by blanchet
fixed MaSh state load code so it works even if the facts are read in disorder
2012-07-18, by blanchet
learn from minimized ATP proofs
2012-07-18, by blanchet
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
2012-07-18, by blanchet
use async manager to manage MaSh learners to make sure they get killed cleanly
2012-07-18, by blanchet
more consolidation of MaSh code
2012-07-18, by blanchet
removed lie
2012-07-18, by blanchet
drastic overhaul of MaSh data structures + fixed a few performance issues
2012-07-18, by blanchet
fixed order of accessibles + other tweaks to MaSh
2012-07-18, by blanchet
added option to control which fact filter is used
2012-07-18, by blanchet
mesh facts by taking into consideration whether a fact is known to MeSh
2012-07-18, by blanchet
implemented meshing of Iter and MaSh results
2012-07-18, by blanchet
implemented MaSh QUERY operation
2012-07-18, by blanchet
refactored MaSh ADD code so it can be used for SUGGEST as well
2012-07-18, by blanchet
implemented low-level MaSh ADD operation
2012-07-18, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
+30000
tip