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
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.
merged
2014-09-02, by boehmes
replay Z3 rewrite steps that lift if-then-else expressions
2014-09-02, by boehmes
test discriminators/selectors in BNF regression suite
2014-09-02, by traytel
merge
2014-09-02, by blanchet
made SML/NJ happier
2014-09-02, by blanchet
tuning
2014-09-02, by blanchet
silenced nonexhaustive primrec warnings
2014-09-02, by traytel
more convenient printing of real numbers after evaluation
2014-09-02, by haftmann
avoid more 'bad background theory' issues
2014-09-01, by blanchet
ported TFL to mixture of old and new datatypes
2014-09-01, by blanchet
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
2014-09-01, by blanchet
ported to use new-style datatypes
2014-09-01, by blanchet
ported Refute to use new datatypes when possible
2014-09-01, by blanchet
renamed BNF theories
2014-09-01, by blanchet
renamed '(BNF_)Constructions_on_Wellorders' to '(BNF_)Wellorder_Constructions'
2014-09-01, by blanchet
added primrec compatibility function
2014-09-01, by blanchet
more work on compatibility interfaces
2014-09-01, by blanchet
added compatibility examples/tests
2014-09-01, by blanchet
implemented compatibility definition of datatype
2014-09-01, by blanchet
implemented compatibility interpretation
2014-09-01, by blanchet
compile
2014-09-01, by blanchet
compile
2014-09-01, by blanchet
tuning
2014-09-01, by blanchet
compile
2014-09-01, by blanchet
more compatibility between old- and new-style datatypes
2014-09-01, by blanchet
added theory-based getters for convenience
2014-09-01, by blanchet
made transfer functions slightly more general
2014-09-01, by blanchet
tuned signatures
2014-09-01, by blanchet
tuning
2014-09-01, by blanchet
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-09-01, by blanchet
tuned structure inclusion
2014-09-01, by blanchet
took out legacy material from 'HOL/Library/Library.thy'
2014-09-01, by blanchet
removed commented out parts
2014-09-01, by blanchet
tuned whitespace
2014-09-01, by blanchet
document 'set_transfer'
2014-09-01, by desharna
generate 'set_transfer' for BNFs
2014-09-01, by desharna
document 'rel_transfer'
2014-09-01, by desharna
generate 'rel_transfer' for BNFs
2014-09-01, by desharna
document 'map_transfer'
2014-09-01, by desharna
note 'map_transfer' more often
2014-09-01, by desharna
separated listsum material
2014-08-31, by haftmann
restored generic value slot, retaining default behaviour and separate approximate command
2014-08-31, by haftmann
convenient printing of (- 1 :: integer) after code evaluation
2014-08-31, by haftmann
inlined unused definition
2014-08-30, by haftmann
add simp rules for divisions of numerals in floor and ceiling.
2014-08-29, by hoelzl
document 'disc_transfer'
2014-08-29, by desharna
generate 'disc_transfer' for (co)datatypes
2014-08-29, by desharna
document 'case_transfer'
2014-08-29, by desharna
generate 'case_transfer' for (co)datatypes
2014-08-29, by desharna
renamed 'skolem' to 'moura' (to suggest Z3-style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
2014-08-28, by blanchet
reworked unskolemization for SPASS
2014-08-28, by blanchet
clarified docs
2014-08-28, by blanchet
gracefully reconstruct Isar proofs in scenarios such as 'using f unfolding g', where backticks can't be used to refer to the unfolded version of 'f' (for some reason)
2014-08-28, by blanchet
prefer '0.2 ms' to '249 \<mu>s'
2014-08-28, by blanchet
use 'thesis' only if it expands to the right thing (it won't after an 'unfolding', for example)
2014-08-28, by blanchet
fixed second computations
2014-08-28, by blanchet
merged minimize and auto_minimize
2014-08-28, by blanchet
pass options to remote Vampire
2014-08-28, by blanchet
removed show stuttering
2014-08-28, by blanchet
generate 'thesis' variable in Sledgehammer Isar proofs
2014-08-28, by blanchet
show microseconds as well (useful when playing with Isar proofs)
2014-08-28, by blanchet
tuned message
2014-08-28, by blanchet
made trace more informative when minimization is enabled
2014-08-28, by blanchet
took out one more occurrence of 'PolyML.makestring'
2014-08-28, by blanchet
try 'skolem' method first for Z3
2014-08-28, by blanchet
tuned tracing output (indirectly)
2014-08-28, by blanchet
going back to bc06471cb7b7 for silencing -- the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
2014-08-28, by blanchet
moved skolem method
2014-08-28, by blanchet
added 'skolem' method, esp. for 'obtain's generated from Z3 proofs
2014-08-28, by blanchet
tuned method description
2014-08-28, by blanchet
three-line 'obtain' format for generated Isar proofs
2014-08-28, by blanchet
tuned;
2014-08-28, by wenzelm
more liberal embedded "text", which includes cartouches;
2014-08-28, by wenzelm
intern xthm only once;
2014-08-28, by wenzelm
tuned terminology
2014-08-28, by blanchet
moved new para to right section of NEWS
2014-08-28, by blanchet
minor NEWS fix
2014-08-28, by blanchet
keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof
2014-08-28, by blanchet
added 'OLD_' prefix in front of old solvers
2014-08-28, by blanchet
updated NEWS
2014-08-28, by blanchet
renamed new SMT module from 'SMT2' to 'SMT'
2014-08-28, by blanchet
updated NEWS
2014-08-28, by blanchet
prefixed all old SMT commands, attributes, etc., with 'old_'
2014-08-28, by blanchet
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
2014-08-28, by blanchet
renaming theory 'Old_SMT'
2014-08-28, by blanchet
moved old setup for SMT out
2014-08-28, by blanchet
moved old 'smt' method out of 'Main'
2014-08-28, by blanchet
reintroduced two-line-per-inference Isar proof format
2014-08-28, by blanchet
removed needless, and for (newer versions of?) Haskell problematic code equations
2014-08-28, by blanchet
removed obsolete RC tags;
2014-08-27, by wenzelm
merged
2014-08-27, by wenzelm
Added tag Isabelle2014 for changeset 8f4a332500e4
2014-08-27, by wenzelm
merged
2014-08-27, by wenzelm
more explicit Method.modifier with reported position;
2014-08-27, by wenzelm
tuned signature -- prefer quasi-abstract Symbol_Pos.source;
2014-08-27, by wenzelm
added ML antiquotation @{source} for Symbol_Pos.source;
2014-08-27, by wenzelm
tuned signature;
2014-08-25, by wenzelm
removed not so interesting 'set_empty'
2014-08-27, by blanchet
avoid 'PolyML.makestring'
2014-08-27, by blanchet
introduce real_of typeclass for real :: 'a => real
2014-08-25, by hoelzl
added lemmas
2014-08-25, by nipkow
better linarith support for floor, ceiling, natfloor, and natceiling
2014-08-19, by hoelzl
add testing framework for generated code
2014-08-25, by Andreas Lochbihler
correct code equation for term_of on integer
2014-08-25, by Andreas Lochbihler
merged
2014-08-25, by Andreas Lochbihler
add code equation for term_of on integer
2014-08-22, by Andreas Lochbihler
added lemmas contributed by Rene Thiemann
2014-08-22, by blanchet
attach modifier only later, to avoid interference as e.g. in "simp add: foo [simplified] bar";
2014-08-22, by wenzelm
tuned whitespace;
2014-08-22, by wenzelm
clarified ML toplevel pp: avoid ML output to be attached to inlined binding positions;
2014-08-22, by wenzelm
merged
2014-08-22, by wenzelm
made SML/NJ happy;
2014-08-22, by wenzelm
clarified Method.section: explicit declaration with static closure;
2014-08-21, by wenzelm
tuned signature -- define some elementary operations earlier;
2014-08-21, by wenzelm
discontinued odd "temporary" workaround from 2006 (6ac7a4fc32a0), which has no measurable relevance;
2014-08-21, by wenzelm
tuned;
2014-08-21, by wenzelm
tuned;
2014-08-21, by wenzelm
tuned;
2014-08-21, by wenzelm
generic euclidean algorithm (due to Manuel Eberl)
2014-08-22, by haftmann
integrated appendix theory into main theory;
2014-08-21, by haftmann
dropped dead file
2014-08-21, by haftmann
fix tactic failure with rel_induct0
2014-08-21, by desharna
added jdk-8u20 (inactive);
2014-08-20, by wenzelm
proper static closure of ML tactic -- data slot is used twice, for ML compiler and transformed declaration;
2014-08-20, by wenzelm
support for declaration within token source;
2014-08-20, by wenzelm
more uniform data slot;
2014-08-20, by wenzelm
default command position is only valid for default text chunk (amending dcb758188aa6);
2014-08-20, by wenzelm
tuned -- more total;
2014-08-20, by wenzelm
tuned;
2014-08-20, by wenzelm
support for nested Token.src within Token.T;
2014-08-20, by wenzelm
tuned signature -- moved type src to Token, without aliases;
2014-08-19, by wenzelm
merged
2014-08-19, by wenzelm
clarified modules;
2014-08-19, by wenzelm
added PARALLEL_ALLGOALS convenience;
2014-08-19, by wenzelm
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
2014-08-19, by wenzelm
tuned signature;
2014-08-19, by wenzelm
more compact datatypes;
2014-08-19, by wenzelm
tuned;
2014-08-19, by wenzelm
clarifed Method.evaluate: turn text into semantic method (like Basic);
2014-08-19, by wenzelm
simplified type Proof.method;
2014-08-19, by wenzelm
more general dummy: may contain "parked arguments", for example;
2014-08-18, by wenzelm
document 'ctr_transfer'
2014-08-19, by desharna
generate 'ctr_transfer' for (co)datatypes
2014-08-19, by desharna
rename Quickcheck_Types to Lattice_Constructions and remove quickcheck setup
2014-08-19, by Andreas Lochbihler
Enum.finite_5 already provides a non-distributive lattice (see 51aa30c9ee4e)
2014-08-19, by Andreas Lochbihler
reduced dependency on 'Datatype' theory and ML module
2014-08-19, by blanchet
removed Z3 3.2, now superseded by Z3 4.3
2014-08-19, by blanchet
avoid old 'smt' method in examples
2014-08-19, by blanchet
robustified tactics
2014-08-19, by blanchet
tuning
2014-08-19, by blanchet
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
2014-08-19, by blanchet
documented slight incompatibility in NEWS
2014-08-19, by blanchet
removed junk
2014-08-18, by blanchet
updated docs
2014-08-18, by blanchet
set attributes on 'set_cases' theorem
2014-08-18, by blanchet
cleaned up derivation of 'sset_induct'
2014-08-18, by blanchet
tuning
2014-08-18, by blanchet
added collection theorem for consistency and convenience
2014-08-18, by blanchet
reordered some (co)datatype property names for more consistency
2014-08-18, by blanchet
document 'map_cong_simp'
2014-08-18, by desharna
generate 'map_cong_simp' for BNFs
2014-08-18, by desharna
merged
2014-08-18, by wenzelm
merged;
2014-08-18, by wenzelm
Added tag Isabelle2014-RC4 for changeset 113b43b84412
Isabelle2014
2014-08-18, by wenzelm
updated to jdk-7u67;
2014-08-18, by wenzelm
postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;
2014-08-17, by wenzelm
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
2014-08-15, by wenzelm
added option editor_syslog_limit;
2014-08-13, by wenzelm
tuned;
2014-08-13, by wenzelm
updated to cygwin-20140813 -- some version after 1.7.31-3;
2014-08-13, by wenzelm
document 'inj_map_strong'
2014-08-18, by desharna
generate 'inj_map_strong' for BNFs
2014-08-18, by desharna
note 'inj_map' more often
2014-08-18, by desharna
generate property 'rel_mono_strong' for BNFs
2014-08-18, by desharna
renamed 'rel_mono_strong' to 'rel_mono_strong0'
2014-08-18, by desharna
use 'image_mset' as BNF map function
2014-08-17, by blanchet
made SML/NJ happy;
2014-08-17, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
clarified order of rules;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
clarified order of arith rules;
2014-08-16, by wenzelm
clarified order of rules for match_tac/resolve_tac;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
updated to named_theorems;
2014-08-16, by wenzelm
modernized module name and setup;
2014-08-16, by wenzelm
updated syntax for localized commands;
2014-08-16, by wenzelm
updated documentation concerning 'named_theorems';
2014-08-16, by wenzelm
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
2014-08-16, by wenzelm
more informative Token.Name with history of morphisms;
2014-08-15, by wenzelm
merged
2014-08-14, by wenzelm
more informative Token.Fact: retain name of dynamic fact (without selection);
2014-08-14, by wenzelm
localized command 'method_setup' and 'attribute_setup';
2014-08-14, by wenzelm
T1 font encoding with searchable underscore (requires proper cm-super fonts);
2014-08-14, by wenzelm
prefer high-level change of \isabellestyle;
2014-08-14, by wenzelm
tuned;
2014-08-14, by wenzelm
tuned;
2014-08-14, by wenzelm
tuned signature;
2014-08-14, by wenzelm
localized method definitions (see also f14c1248d064);
2014-08-14, by wenzelm
tuned signature -- prefer self-contained user-space tool;
2014-08-14, by wenzelm
document property 'rel_map'
2014-08-14, by desharna
generate 'rel_map' theorem for BNFs
2014-08-14, by desharna
tuned;
2014-08-13, by wenzelm
merged
2014-08-13, by wenzelm
tuned signature -- proper Local_Theory.add_thms_dynamic;
2014-08-13, by wenzelm
transfer result of Global_Theory.add_thms_dynamic to context stack;
2014-08-13, by wenzelm
localized attribute definitions;
2014-08-13, by wenzelm
load local_theory.ML before attrib.ML, with subtle change of semantics due to canonical Local_Theory.map_contexts instead of private Local_Theory.map_top;
2014-08-13, by wenzelm
clarified terminology: first is top (amending d110b0d1bc12);
2014-08-13, by wenzelm
tuned whitespace;
2014-08-13, by wenzelm
tuned comments;
2014-08-13, by wenzelm
add algebraic type class instances for Enum.finite* types
2014-08-13, by Andreas Lochbihler
Quickcheck_Types is no longer needed due to 51aa30c9ee4e
2014-08-13, by Andreas Lochbihler
clarified focus and key handling -- more like SideKick;
2014-08-12, by wenzelm
merged
2014-08-12, by wenzelm
tuned signature according to Scala version -- prefer explicit argument;
2014-08-12, by wenzelm
tuned signature;
2014-08-12, by wenzelm
generic process wrapping in Prover;
2014-08-12, by wenzelm
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
2014-08-12, by wenzelm
allow hyperlinks without offset, just in case the prover emits such reports, despite Position.is_reported;
2014-08-12, by wenzelm
more frugal standard message properties;
2014-08-12, by wenzelm
tuned;
2014-08-12, by wenzelm
clarified Position.Identified: do not require range from prover, default to command position;
2014-08-12, by wenzelm
maintain Command_Range position as in ML;
2014-08-12, by wenzelm
more compact representation of special string values;
2014-08-12, by wenzelm
separate Java FX modules -- no need to include jfxrt.jar by default;
2014-08-12, by wenzelm
tuned signature;
2014-08-12, by wenzelm
tuned signature;
2014-08-12, by wenzelm
separate module Command_Span: mostly syntactic representation;
2014-08-12, by wenzelm
tuned signature;
2014-08-11, by wenzelm
clarified Command_Span in accordance to Scala (see also c2c1e5944536);
2014-08-11, by wenzelm
tuned output, in accordance to transaction name in ML;
2014-08-11, by wenzelm
more explicit type Span in Scala, according to ML version;
2014-08-11, by wenzelm
clarified modules;
2014-08-11, by wenzelm
clarified signature: entity serial number is not position id;
2014-08-11, by wenzelm
avoid needless (and wrong w.r.t. sorts) generation of type variables; tuned whitespaces;
2014-08-12, by blanchet
improved unfolding of 'let's
2014-08-12, by blanchet
tuned whitespace
2014-08-12, by blanchet
less aggressive unfolding; removed debugging;
2014-08-12, by blanchet
document property 'set_cases'
2014-08-12, by desharna
generate 'set_cases' theorem for (co)datatypes
2014-08-12, by desharna
document property 'set_intros'
2014-08-12, by desharna
generate 'set_intros' theorem for (co)datatypes
2014-08-12, by desharna
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
2014-08-11, by traytel
reduced warnings;
2014-08-10, by wenzelm
some localization;
2014-08-10, by wenzelm
support aliases within the facts space;
2014-08-10, by wenzelm
support for named collections of theorems in canonical order;
2014-08-10, by wenzelm
insist in proper 'document_files';
2014-08-10, by wenzelm
tuned -- avoid confusion with @{assert} for system failures (exception Fail);
2014-08-10, by wenzelm
tuned -- eliminated redundant check (see 1f77110c94ef);
2014-08-10, by wenzelm
merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
2014-08-10, by wenzelm
updated URL (anticipate merge with 85b8cc142384);
2014-08-10, by wenzelm
Added tag Isabelle2014-RC3 for changeset 91e188508bc9
2014-08-10, by wenzelm
proper layered_pane for JDialog, e.g. relevant for floating dockables in jEdit, for completion popup in text field;
2014-08-10, by wenzelm
follow link to originating command, to ensure that Simplifier_Trace_Dockable displays its results (via current_command);
2014-08-10, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned comments;
2014-08-09, by wenzelm
clarified synchronized scope;
2014-08-09, by wenzelm
tuned comments;
2014-08-09, by wenzelm
application manifest for Windows 8/8.1 dpi scaling;
2014-08-08, by wenzelm
observe context visibility -- less redundant warnings;
2014-08-08, by wenzelm
improved monitor panel;
2014-08-08, by wenzelm
protocol command for heap management, e.g. in Isabelle/jEdit/Scala console: PIDE.session.protocol_command("ML_System.share_common_data");
2014-08-05, by wenzelm
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
2014-08-05, by wenzelm
obsolete (see f7700146678d);
2014-08-05, by wenzelm
tuned proofs -- fewer warnings;
2014-08-05, by wenzelm
clarified Element.init vs. Element.init' -- the latter also avoids redundant warnings due to declatations when preparing locale expressions / interpretations;
2014-08-05, by wenzelm
avoid duplication of warnings stemming from simp/intro declarations etc.;
2014-08-05, by wenzelm
tuned proofs;
2014-08-05, by wenzelm
restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;
2014-08-05, by wenzelm
tuned;
2014-08-05, by wenzelm
more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
2014-08-05, by wenzelm
refined context visibility again (amending f5f9fad3321c, 8e3e004f1c31): avoid spurious warning due to global config options;
2014-08-05, by wenzelm
even more thorough reset on mouse drag (see also 0c63f3538639, 7e8c11011fdf);
2014-08-04, by wenzelm
tuned;
2014-08-04, by wenzelm
tuned;
2014-08-04, by wenzelm
Added tag Isabelle2014-RC2 for changeset ee908fccabc2
2014-08-04, by wenzelm
more user aliases;
2014-08-04, by wenzelm
registered Haskabelle-2014
2014-08-04, by noschinl
tuned, so codegen runs with current isabelle again
2014-08-01, by Lars Noschinski
tuned whitespace;
2014-08-03, by wenzelm
more robust popup geometry vs. formatted margin;
2014-08-03, by wenzelm
tuned message;
2014-08-03, by wenzelm
updated URL;
2014-08-02, by wenzelm
tuned;
2014-08-02, by wenzelm
updated URL;
2014-08-02, by wenzelm
more emphatic warning via error_message (violating historic TTY protocol);
2014-08-02, by wenzelm
proper priority for error over warning also for node_status (see 9c5220e05e04);
2014-08-02, by wenzelm
more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
2014-08-02, by wenzelm
always resolve symlinks for local files, e.g. relevant for ML_file to load proper source via editor instead of stored file via prover;
2014-08-02, by wenzelm
tuned output;
2014-08-02, by wenzelm
prefer non-strict Execution.print, e.g relevant for redirected ML compiler reports after error (see also e79f76a48449 and 40274e4f5ebf);
2014-08-01, by wenzelm
careful when calling 'Thm.proof_body_of' -- it can throw exceptions
2014-08-01, by blanchet
removed unused stuff;
2014-08-01, by wenzelm
agree on keyword categories with ML;
2014-08-01, by wenzelm
more keyword categories (as in ML);
2014-08-01, by wenzelm
prefer dynamic ML_print_depth if context happens to be available;
2014-07-31, by wenzelm
completion popup supports both ENTER and TAB (default);
2014-07-31, by wenzelm
clarified compile-time use of ML_print_depth;
2014-07-31, by wenzelm
more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;
2014-07-31, by wenzelm
correctly resolve selector names in default value equations
2014-07-30, by blanchet
update documentation for Lifting/Transfer
2014-07-30, by kuncar
add Isabelle Datatype Manual to the bibliography
2014-07-30, by kuncar
CONTRIBUTORS;
2014-07-30, by wenzelm
NEWS
2014-07-30, by kuncar
better ordering of positive_integral renaming to nn_integral in NEWS
2014-07-29, by hoelzl
made tactic more robust w.r.t. dead variables; tuned;
2014-07-28, by desharna
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
2014-07-27, by blanchet
some actual workaround to remove document nodes;
2014-07-28, by wenzelm
Added tag Isabelle2014-RC1 for changeset c0fd03d13d28
2014-07-27, by wenzelm
tuned;
2014-08-09, by wenzelm
tuned
2014-08-09, by nipkow
add complete_lattice instances for Enum.finite_* types such that quickcheck deals with lattice class operations
2014-08-08, by Andreas Lochbihler
tuned
2014-08-08, by nipkow
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
2014-08-07, by blanchet
generate nicer 'set' theorems for (co)datatypes
2014-08-07, by blanchet
compile
2014-08-07, by blanchet
took out test driver
2014-08-07, by blanchet
make TPTP tools work on polymorphic (TFF1) problems as well
2014-08-07, by blanchet
put comments between TPTP lines to comply with TPTP BNF
2014-08-07, by blanchet
test driver
2014-08-07, by blanchet
treat variables as frees in 'conjecture's
2014-08-07, by blanchet
support TFF1 in TPTP parser/interpreter
2014-08-07, by blanchet
tuning
2014-08-07, by blanchet
tuned
2014-08-07, by traytel
tuned
2014-08-07, by nipkow
tuned
2014-08-07, by nipkow
merged
2014-08-06, by traytel
handle deep nesting in N2M
2014-08-06, by traytel
made tactic more robust
2014-08-06, by traytel
added lemma
2014-08-06, by nipkow
replaced misleading - by _
2014-08-06, by nipkow
more correct clique computation for N2M
2014-08-05, by blanchet
regenerated ML-Lex/Yacc files
2014-08-05, by blanchet
correctly interpret arithmetic types
2014-08-05, by blanchet
added 'datatype_compat' tests
2014-08-05, by blanchet
tuning whitespace
2014-08-05, by blanchet
tuned skolemization
2014-08-05, by blanchet
rationalize Skolem names
2014-08-05, by blanchet
tuning
2014-08-05, by blanchet
tuned code
2014-08-05, by blanchet
don't rename variables which will be renamed later anyway
2014-08-05, by blanchet
normalize skolem argument variable names so that they coincide when taking the conjunction
2014-08-05, by blanchet
tuning
2014-08-05, by blanchet
tuned comments
2014-08-04, by blanchet
deal with E definitions
2014-08-04, by blanchet
updated 'compress' docs
2014-08-04, by blanchet
cleaner 'compress' option
2014-08-04, by blanchet
renamed 'sh_minimize' to 'minimize'; compile;
2014-08-04, by blanchet
restored more sorting
2014-08-04, by blanchet
tuned terminology (cf. 'isar_proofs' option)
2014-08-04, by blanchet
sort facts in minimizer as well
2014-08-04, by blanchet
default on 'metis' for ATPs if preplaying is disabled
2014-08-04, by blanchet
more informative preplay failures
2014-08-04, by blanchet
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
2014-08-04, by blanchet
slightly earlier exit from preplaying
2014-08-04, by blanchet
honor 'dont_minimize' option when preplaying one-liner proof
2014-08-04, by blanchet
Metis is being used to emulate E steps;
2014-06-22, by sultana
updated application of print_tac to take context parameter;
2014-06-22, by sultana
better duplicate detection
2014-08-02, by blanchet
normalize conjectures vs. negated conjectures when comparing terms
2014-08-01, by blanchet
tweaked 'clone' formula detection
2014-08-01, by blanchet
fine-tuned Isar reconstruction, esp. boolean simplifications
2014-08-01, by blanchet
centralized boolean simplification so that e.g. LEO-II benefits from it
2014-08-01, by blanchet
careful when compressing 'obtains'
2014-08-01, by blanchet
better handling of variable names
2014-08-01, by blanchet
try to get rid of skolems first
2014-08-01, by blanchet
nicer generated variable names
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
no need to 'obtain' variables not in formula
2014-08-01, by blanchet
more precise handling of LEO-II skolemization
2014-08-01, by blanchet
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
peek instead of joining -- is perhaps less risky
2014-08-01, by blanchet
export ML function
2014-08-01, by blanchet
compile
2014-08-01, by blanchet
removed 'metisFT' support in Mirabelle
2014-08-01, by blanchet
removed Mirabelle minimization code
2014-08-01, by blanchet
modernized Mirabelle (a bit) and made it compile
2014-08-01, by blanchet
restored a bit of laziness
2014-08-01, by blanchet
reorder quantifiers to ease Z3 skolemization
2014-08-01, by blanchet
tuned order of arguments
2014-08-01, by blanchet
tuned name context code
2014-08-01, by blanchet
tuned whitespace
2014-08-01, by blanchet
more rational unskolemizing of names
2014-08-01, by blanchet
added appropriate method for skolemization of Z3 steps to the mix
2014-08-01, by blanchet
pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared)
2014-08-01, by blanchet
honor 'try0' also for one-liners
2014-08-01, by blanchet
tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence
2014-08-01, by blanchet
further minimize one-liner
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
eliminated needlessly complex message tail
2014-08-01, by blanchet
updated NEWS
2014-08-01, by blanchet
update documentation after removal of 'min' subcommand
2014-08-01, by blanchet
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
2014-08-01, by blanchet
rationalized preplaying by eliminating (now superfluous) laziness
2014-08-01, by blanchet
removed proof methods as provers from docs
2014-08-01, by blanchet
simplified minimization logic
2014-08-01, by blanchet
tuning
2014-08-01, by blanchet
remove lambda-lifting related assumptions from generated Isar proofs
2014-08-01, by blanchet
whitespace tuning
2014-08-01, by blanchet
remove YXML formatting when parsing backquoted facts supplied manually to Sledgehammer
2014-08-01, by blanchet
generate backquotes without markup, since this confuses preplay; bump up spying version identifier;
2014-08-01, by blanchet
simplified tactics slightly
2014-07-31, by traytel
cascading timeout in parallel evaluation, to rapidly find optimum
2014-07-31, by blanchet
put faster proof methods first
2014-07-30, by blanchet
use parallel preplay machinery also for one-line proofs
2014-07-30, by blanchet
updated docs
2014-07-30, by blanchet
always minimize Sledgehammer results by default
2014-07-30, by blanchet
tuned ML function name
2014-07-30, by blanchet
reduced preplay timeout to 1 s
2014-07-30, by blanchet
added more proof methods for one-liners
2014-07-30, by blanchet
unlift before uncombine, because the definition of a lambda-lifted symbol might have an SK combinator in it (in hybrid encodings)
2014-07-30, by blanchet
Improving robustness and indentation corrections.
2014-07-30, by fleury
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
2014-07-30, by fleury
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
2014-07-30, by fleury
Whitespace and indentation correction.
2014-07-30, by fleury
Simplifying the labels in the proof of the SMT solver veriT.
2014-07-30, by fleury
Changing ~ into - for unuary minus (not supported by veriT)
2014-07-30, by fleury
imported patch satallax_skolemization_in_tree_part
2014-07-30, by fleury
imported patch hilbert_choice_support
2014-07-30, by fleury
veriT changes for lifted terms, and ite_elim rules.
2014-07-30, by fleury
imported patch satallax_proof_support_Sledgehammer
2014-07-30, by fleury
Basic support for the higher-order ATP Satallax.
2014-07-30, by fleury
Subproofs for the SMT solver veriT.
2014-07-30, by fleury
Basic support for the SMT prover veriT.
2014-07-30, by fleury
removing the '= True' generated by Leo-II.
2014-07-30, by fleury
Skolemization support for leo-II and Zipperposition.
2014-07-30, by fleury
document property 'set_induct'
2014-07-30, by desharna
generate 'set_induct' theorem for codatatypes
2014-07-30, by desharna
also try 'metis' with 'full_types'
2014-07-30, by blanchet
header tuning
2014-07-29, by blanchet
correctly translate THF functions from terms to types
2014-07-28, by blanchet
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
2014-07-27, by blanchet
back to post-release mode -- after fork point;
2014-07-27, by wenzelm
tuned;
2014-07-27, by wenzelm
tuned;
2014-07-27, by wenzelm
no -optimise -- produces bad bytecode;
2014-07-26, by wenzelm
output state first -- avoid fluctuation wrt. warnings, errors, etc.;
2014-07-26, by wenzelm
tuned comment;
2014-07-25, by wenzelm
updated to polyml-5.5.2-1 which addresses two hard crashes;
2014-07-25, by wenzelm
updated to cygwin-20140725, which is presumably close to Cygwin 1.7.31-1;
2014-07-25, by wenzelm
added more functions and lemmas
2014-07-25, by nipkow
proper mkdir;
2014-07-25, by wenzelm
proper option -O;
2014-07-25, by wenzelm
some reshuffling of Poly/ML version to evade failing tests;
2014-07-25, by wenzelm
old 'defs' is legacy --- slightly odd side-entry that bypasses regular Local_Theory.define interface;
2014-07-25, by wenzelm
proper volume name, such that background image is found in /Volumes/Isabelle/.background;
2014-07-25, by wenzelm
tuned;
2014-07-25, by wenzelm
tuned message;
2014-07-25, by wenzelm
setup for drag-and-drop DMG;
2014-07-25, by wenzelm
merge
2014-07-25, by blanchet
reordered provers
2014-07-25, by blanchet
compile
2014-07-25, by blanchet
faster minimization by not adding facts that are already in the simpset
2014-07-25, by blanchet
added missing facts to proof method
2014-07-25, by blanchet
don't lose 'minimize' flag before it reaches Isar proof text generation
2014-07-25, by blanchet
tuning
2014-07-25, by blanchet
avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
2014-07-25, by blanchet
compile
2014-07-25, by blanchet
more robustness in Isar proof construction
2014-07-25, by blanchet
tuning
2014-07-25, by blanchet
merged
2014-07-24, by wenzelm
more elementary exception handling: evade hard crash of (Runtime.thread true undefined) on Poly/ML 5.5.1 and 5.5.2;
2014-07-24, by wenzelm
tuned code
2014-07-24, by blanchet
having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations
2014-07-24, by kuncar
store explicitly quotient types with no_code => more precise registration of code equations
2014-07-24, by kuncar
don't needlessly regenerate entire file when the time stamps are equal
2014-07-24, by blanchet
eliminated source of 'DUP's in MaSh
2014-07-24, by blanchet
fixed sorting (broken since 9cc802a8ab06)
2014-07-24, by blanchet
reenabled MaSh for Isabelle2014 release (hopefully)
2014-07-24, by blanchet
beware of duplicate fact names
2014-07-24, by blanchet
refined filter for ATP steps to avoid 'have True' steps in E proofs
2014-07-24, by blanchet
filter out 'theory(...)' from dependencies early on
2014-07-24, by blanchet
introduce fact chaining also under first step
2014-07-24, by blanchet
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
2014-07-24, by blanchet
merged
2014-07-24, by wenzelm
proper perl;
2014-07-24, by wenzelm
less warnings -- ignore potential prover startup/shutdown races;
2014-07-24, by wenzelm
tuned spelling;
2014-07-24, by wenzelm
further distinction of Isabelle distribution: alert for identified release candidates;
2014-07-24, by wenzelm
updated to scala-2.11.2;
2014-07-24, by wenzelm
clarified file names;
2014-07-24, by wenzelm
less ambitious isatest, avoid "Exception- InternalError: Backing up too far (32bit) raised while compiling" in polyml-5.4.1;
2014-07-24, by wenzelm
tuned imports;
2014-07-24, by wenzelm
proper scope of comments;
2014-07-24, by wenzelm
make SML/NJ happy;
2014-07-24, by wenzelm
prevent beta-contraction in proving extra assumptions for abs_eq
2014-07-24, by kuncar
more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy);
2014-07-24, by wenzelm
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
2014-07-24, by wenzelm
tuned;
2014-07-24, by wenzelm
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
2014-07-24, by wenzelm
updated NEWS according to d38a98f496dd (see also bdc2c6b40bf2);
2014-07-24, by wenzelm
stick to external proofs when invoking E, because they are more detailed and do not merge steps
2014-07-24, by blanchet
more robust handling of types for skolems (modeled as Frees)
2014-07-24, by blanchet
tuning
2014-07-24, by blanchet
repaired named derivations
2014-07-24, by blanchet
use the noted theorems in 'BNF_Comp'
2014-07-24, by blanchet
use the noted theorem whenever possible, also in 'BNF_Def'
2014-07-24, by blanchet
use termtab instead of (perhaps overly sensitive) thmtab
2014-07-24, by blanchet
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
2014-07-24, by blanchet
tuned message;
2014-07-23, by wenzelm
added action "isabelle.options" (despite problems with initial window size);
2014-07-23, by wenzelm
more official Thy_Info.script_thy;
2014-07-23, by wenzelm
more frugal edits;
2014-07-23, by wenzelm
enable hires explictly, as seen for other high-end Java applications on the Web;
2014-07-23, by wenzelm
more markup;
2014-07-23, by wenzelm
another attempt at more aggressive auto-loading (amending af28fdd50690) -- hidden buffers are now suppressed;
2014-07-23, by wenzelm
more frugal edits;
2014-07-23, by wenzelm
more explicit treatment of cleared nodes (removal is implicit);
2014-07-23, by wenzelm
clarified display;
2014-07-23, by wenzelm
more workarounds for scalac;
2014-07-23, by wenzelm
clarified display;
2014-07-23, by wenzelm
avoid redundant data structure;
2014-07-23, by wenzelm
more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-07-23, by wenzelm
tuned;
2014-07-23, by wenzelm
tuned comments;
2014-07-23, by wenzelm
clarified module name: facilitate alternative GUI frameworks;
2014-07-23, by wenzelm
proper change of perspective for removed nodes (stemming from closed buffers);
2014-07-23, by wenzelm
tuned signature;
2014-07-23, by wenzelm
some robustification of console output;
2014-07-22, by wenzelm
updated ErrorList.jar;
2014-07-22, by wenzelm
discontinued presumable workarounds for extra inter-theory space, which are obsolete since 0e5fa27d3293;
2014-07-22, by wenzelm
evade problems with MikTeX on Windows;
2014-07-22, by wenzelm
tuned messages;
2014-07-22, by wenzelm
support multiple selected print operations instead of slightly odd "menu";
2014-07-22, by wenzelm
more default imports;
2014-07-22, by wenzelm
no keyword completion within word context -- especially avoid its odd visual rendering;
2014-07-22, by wenzelm
merged
2014-07-22, by Andreas Lochbihler
merged
2014-07-21, by Andreas Lochbihler
add parametricity lemmas
2014-07-21, by Andreas Lochbihler
add lemma
2014-07-21, by Andreas Lochbihler
merged
2014-07-21, by wenzelm
refer to Simplifier Trace panel on first invocation;
2014-07-21, by wenzelm
removed unused markup (cf. 2f7d91242b99);
2014-07-21, by wenzelm
regular message to refer to Simplifier Trace panel (unused);
2014-07-21, by wenzelm
proper Swing buttons instead of active areas within text (by Lars Hupel);
2014-07-21, by wenzelm
misc tuning and simplification;
2014-07-21, by wenzelm
clarified "simp_trace_new" and corresponding isar-ref section;
2014-07-21, by wenzelm
more on "Simplifier trace" (by Lars Hupel);
2014-07-21, by wenzelm
always complete explicit symbols;
2014-07-21, by wenzelm
discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
2014-07-21, by wenzelm
updated to jdk-7u65;
2014-07-21, by wenzelm
regression test for datatypes defined in IsaFoR
2014-07-21, by traytel
ghc mac installation repaired; test back on.
2014-07-21, by kleing
proper condition wrt. ISABELLE_GHC (cf. 8840fa17e17c);
2014-07-20, by wenzelm
updated to jdk-8u11 (inactive);
2014-07-20, by wenzelm
avoid delay_load overrun;
2014-07-20, by wenzelm
provide explicit options file -- avoid multiple Scala/JVM invocation;
2014-07-20, by wenzelm
check and build Isabelle session for console tool -- avoid multiple Scala/JVM invocation;
2014-07-20, by wenzelm
attempt to run without ISABELLE_GHC setting again on mac-poly
2014-07-19, by kleing
apparently, setting ISABELLE_GHC makes ghc unusable
2014-07-19, by kleing
reverse induction over nonempty lists
2014-07-19, by haftmann
more appropriate postprocessing of rational numbers: extract sign to front of fraction
2014-07-19, by haftmann
doc fixes (contributed by Christian Sternagel)
2014-07-19, by blanchet
made SML/NJ happier
2014-07-19, by blanchet
avoid duplicate fact name
2014-07-18, by kleing
afp-poly runs on macbroy2 (different ghc)
2014-07-18, by kleing
reinstated popular add_ac and mult_ac to avoid needless incompatibilities in user space
2014-07-18, by nipkow
tuned
2014-07-18, by nipkow
register tree with datatype_compat ot support QuickCheck
2014-07-17, by hoelzl
fix bug caused by bad context
2014-07-17, by desharna
add mk_Trueprop_mem utility function
2014-07-17, by desharna
disabled MaSh for the Isabelle2014 release, due to a couple of issues
2014-07-16, by blanchet
refactor commonly used functions
2014-07-16, by desharna
document property 'rel_sel'
2014-07-16, by desharna
generate 'rel_sel' theorem for (co)datatypes
2014-07-16, by desharna
fix rel_cases
2014-07-16, by desharna
made SML/NJ happier
2014-07-15, by blanchet
add ISABELLE_GHC settings for isatest
2014-07-15, by kleing
mira.py: building jEdit plugin is required for makeall
2014-07-14, by noschinl
took out 'rel_cases' for now because of failing tactic
2014-07-15, by blanchet
record MaSh algorithm in spying data
2014-07-15, by blanchet
tuned whitespace (also in strings)
2014-07-15, by blanchet
also learn when 'fact_filter =' is set explicitly
2014-07-15, by blanchet
no warning in case MaSh is disabled
2014-07-15, by blanchet
don't generate a 'set-logic' command when generating problems in a non-standard (but Z3-supported) union-of-everything logic
2014-07-15, by blanchet
no need for 'mash' subdirectory after removal of Python program
2014-07-15, by blanchet
fix typo
2014-07-14, by panny
throw error for bad input
2014-07-14, by panny
catch "not found" case
2014-07-14, by panny
merge
2014-07-12, by blanchet
don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax
2014-07-12, by blanchet
tuning
2014-07-12, by blanchet
made SML/NJ happier
2014-07-12, by blanchet
reactivate session Quickcheck_Examples
2014-07-11, by Andreas Lochbihler
adapt and reactivate Quickcheck_Types and add two test cases
2014-07-11, by Andreas Lochbihler
more docs
2014-07-11, by blanchet
lambda-lifting for Z3 Isar proofs
2014-07-10, by blanchet
append instead of prepend lambda-lifted definitions -- this eases reconstruction in veriT (outside repository)
2014-07-10, by blanchet
avoid loop in 'all_class_pairs' (caused by e.g. loading the 'Ceta' theory and calling Sledgehammer with the two facts 'fun_of_map.cases' and 'Lattices.bounded_lattice_top_class.sup_top_left' with a polymorphic type encoding)
2014-07-10, by blanchet
merged
2014-07-09, by nipkow
added lemmas
2014-07-09, by nipkow
improved docs
2014-07-09, by blanchet
made SML/NJ happier
2014-07-09, by blanchet
got rid of a pointer equality
2014-07-09, by blanchet
get rid of some pointer equalities
2014-07-09, by blanchet
tuned terminology
2014-07-09, by blanchet
improvements to the machine learning algos (due to Cezary K.)
2014-07-09, by blanchet
added lemma
2014-07-07, by nipkow
refactor some tactics
2014-07-07, by desharna
refactor some tactics
2014-07-07, by desharna
add helper function map_prod
2014-07-07, by desharna
document property 'rel_cases'
2014-07-07, by desharna
generate 'rel_cases' theorem for (co)datatypes
2014-07-07, by desharna
update for release;
2014-07-05, by wenzelm
Added tag Isabelle2014-RC0 for changeset 251ef0202e71
2014-07-05, by wenzelm
merged
2014-07-05, by wenzelm
modernized definitions;
2014-07-05, by wenzelm
proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);
2014-07-05, by wenzelm
CONTRIBUTORS
2014-07-05, by haftmann
refrain from auxiliary abbreviation: be more explicit to the reader in situations where syntax translation does not apply;
2014-07-05, by haftmann
misc tuning for release;
2014-07-05, by wenzelm
tuned;
2014-07-05, by wenzelm
NEWS
2014-07-05, by haftmann
prefer ac_simps collections over separate name bindings for add and mult
2014-07-05, by haftmann
added Tom's hyp_subst update
2014-07-05, by kleing
reduced name variants for assoc and commute on plus and mult
2014-07-04, by haftmann
tuned;
2014-07-04, by wenzelm
insist in explicit overloading;
2014-07-04, by wenzelm
more uniform names;
2014-07-04, by wenzelm
misc tuning for release;
2014-07-04, by wenzelm
revived unchecked theory (see cebaf814ca6e);
2014-07-04, by wenzelm
suppress completion of obscure keyword;
2014-07-04, by wenzelm
tuned;
2014-07-04, by wenzelm
misc tuning for release;
2014-07-04, by wenzelm
NEWS;
2014-07-04, by wenzelm
Tail recursion no longer supported by "function".
2014-07-03, by nipkow
merged
2014-07-03, by haftmann
weaker assumption for "list_emb_trans"; added lemma
2014-07-03, by Christian Sternagel
added monotonicity lemma for list embedding
2014-07-03, by Christian Sternagel
no built-in reflexivity of list embedding (which is more standard; now embedding is reflexive whenever the base-order is)
2014-07-03, by Christian Sternagel
renamed "list_hembeq" into slightly shorter "list_emb"
2014-07-03, by Christian Sternagel
misc tuning;
2014-07-03, by wenzelm
merge
2014-07-03, by desharna
document property 'rel_intros'
2014-07-03, by desharna
generate 'rel_intros' theorem for (co)datatypes
2014-07-03, by desharna
Hypsubst preserves equality hypotheses
2014-06-11, by Thomas Sewell
tuned grammar and spelling (cf. 0cf15843b82f);
2014-07-02, by wenzelm
document property 'corec_code'
2014-07-02, by desharna
generate 'corec_code' theorem for codatatypes
2014-07-02, by desharna
modernized definitions;
2014-07-02, by wenzelm
misc tuning and clarification;
2014-07-02, by wenzelm
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
2014-07-02, by wenzelm
optional exit hook for theory-like targets
2014-07-02, by haftmann
restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game
2014-07-02, by haftmann
centralized (ad-hoc) switching of targets in named_target.ML
2014-07-02, by haftmann
add lemmas: polynomial div/mod distribute over addition
2014-07-01, by huffman
reverted 9512b867259c -- appears to break 'metis'
2014-07-01, by blanchet
clarified "axiomatization" -- minor rewording of this delicate concept;
2014-07-01, by wenzelm
tuned;
2014-07-01, by wenzelm
more on ML options;
2014-07-01, by wenzelm
redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
2014-07-01, by wenzelm
overdue NEWS concerning c4daa97ac57a
2014-07-01, by immler
Merge
2014-07-01, by paulson
for new release
2014-07-01, by paulson
merge
2014-07-01, by desharna
document property 'rel_induct'
2014-07-01, by desharna
generate 'rel_induct' theorem for datatypes
2014-07-01, by desharna
fixed soundness bug in monotonicity-based type encodings -- the helper facts must be considered too
2014-07-01, by blanchet
added hidden check to Sledgehammer fact filters, to avoid picking up facts like 'Nat.nat_induct0'
2014-07-01, by blanchet
whitespace tuning
2014-07-01, by blanchet
robustness in the face of ill-typed "unchecked" terms (e.g. case expressions)
2014-07-01, by blanchet
use context instead of theory
2014-07-01, by blanchet
fine-tuned methods
2014-07-01, by blanchet
tuned message
2014-07-01, by blanchet
updated docs
2014-07-01, by blanchet
changed default MaSh engine
2014-07-01, by blanchet
removed needless code
2014-07-01, by blanchet
speed up MaSh a bit
2014-07-01, by blanchet
mix NB and kNN
2014-07-01, by blanchet
tuned (reordered) code
2014-07-01, by blanchet
clean up MaSh export a bit
2014-07-01, by blanchet
clean up MaSh evaluation driver
2014-07-01, by blanchet
merged
2014-07-01, by wenzelm
tuned;
2014-07-01, by wenzelm
clarified quasi-generic PIDE;
2014-07-01, by wenzelm
misc updates for release;
2014-07-01, by wenzelm
more release notes;
2014-07-01, by wenzelm
Library/Tree: bst is preferred to be a function
2014-07-01, by hoelzl
Library/Tree: use datatype_new, bst is an inductive predicate
2014-07-01, by hoelzl
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
2014-06-30, by hoelzl
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
2014-06-30, by hoelzl
some lemmas about the indicator function; removed lemma sums_def2
2014-06-30, by hoelzl
generate type correct terms in uncheck phase
2014-07-01, by traytel
updated to sumatra_pdf-2.5.2;
2014-06-30, by wenzelm
ProofGeneral-4.2-2 is optional component (including the traditional helper scripts);
2014-06-30, by wenzelm
removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
2014-06-30, by wenzelm
tuned comments;
2014-06-30, by wenzelm
updated README;
2014-06-30, by wenzelm
"isabelle tty" is superseded by "isabelle console";
2014-06-30, by wenzelm
tuned description: fit into 80 chars terminal;
2014-06-30, by wenzelm
qualified String.explode and String.implode
2014-06-30, by haftmann
removed non-existing MaSh component from list
2014-06-29, by blanchet
modernized diagnostic options
2014-06-29, by haftmann
use SMT2
2014-06-29, by blanchet
compile
2014-06-29, by blanchet
tuning
2014-06-29, by blanchet
killed Python version of MaSh, now that the SML version works adequately
2014-06-29, by blanchet
tracing facilities for the code generator preprocessor
2014-06-28, by haftmann
tuned interface
2014-06-28, by haftmann
corrected handled exception
2014-06-28, by haftmann
proper trading of variables;
2014-06-28, by haftmann
modernized
2014-06-28, by haftmann
jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;
2014-06-28, by wenzelm
removed slightly odd fall-back on complete-word (NB: connection to default menu action is unclear);
2014-06-28, by wenzelm
updated NEWS -- removed material that is already in the manual;
2014-06-28, by wenzelm
merged
2014-06-28, by wenzelm
misc tuning;
2014-06-28, by wenzelm
misc tuning;
2014-06-28, by wenzelm
CONTRIBUTORS
2014-06-28, by haftmann
fact consolidation
2014-06-28, by haftmann
more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
2014-06-27, by wenzelm
merged
2014-06-27, by wenzelm
command 'print_term_bindings' supersedes 'print_binds';
2014-06-27, by wenzelm
Proof General legacy;
2014-06-27, by wenzelm
removed obsolete "isabelle unsymbolize";
2014-06-27, by wenzelm
minor renovation of slightly odd and old README;
2014-06-27, by wenzelm
sane environment defaults for Mac OS X, based on former App1/script -- e.g. relevant for MacTeX PATH;
2014-06-27, by wenzelm
tweaking
2014-06-27, by blanchet
correctly take weights into consideration
2014-06-27, by blanchet
tuned whitespace and parentheses
2014-06-27, by blanchet
use right theory name for theorems in evaluation driver
2014-06-27, by blanchet
killed dead code
2014-06-27, by blanchet
reintroduced 'extra features' + only print message in verbose mode
2014-06-27, by blanchet
got rid of hard-coded weights, now that we have TFIDF
2014-06-27, by blanchet
tuning
2014-06-27, by blanchet
tuning
2014-06-27, by blanchet
reintroduced 'extra features' but with lower weight than before (to account for tfidf)
2014-06-27, by blanchet
resolution modulo double negation
2014-06-27, by blanchet
compile
2014-06-27, by blanchet
merged two small theory files
2014-06-27, by blanchet
tuned variable names
2014-06-27, by blanchet
whitespace tuning
2014-06-27, by blanchet
repaired BNF 'size' generation tactic for datatypes mixng old- and new-style datatypes on the right-hand side
2014-06-27, by blanchet
tiny refinements
2014-06-27, by paulson
suppress documentation "how_to_prove_it" for now, notably for release;
2014-06-26, by wenzelm
updated to jdk-7u60 -- back to stable Java 7 for Isabelle2014 release;
2014-06-26, by wenzelm
updated generated file;
2014-06-26, by wenzelm
merged
2014-06-26, by wenzelm
updated cygwin on server;
2014-06-26, by wenzelm
tuning
2014-06-26, by blanchet
reintroduced MaSh hints, this time as persistent creatures
2014-06-26, by blanchet
always expand all paths
2014-06-26, by blanchet
tuned output
2014-06-26, by blanchet
tuned output
2014-06-26, by blanchet
right array indexing
2014-06-26, by blanchet
incremental learning when learing several facts
2014-06-26, by blanchet
tuning
2014-06-26, by blanchet
more incremental learning of single fact
2014-06-26, by blanchet
avoid needless (trivial) reordering on load
2014-06-26, by blanchet
recompute learning data at learning time, not query time
2014-06-26, by blanchet
imported patch killed_num_known_facts0
2014-06-26, by blanchet
refactoring
2014-06-26, by blanchet
renamed experimental learning engines
2014-06-26, by blanchet
tuning
2014-06-26, by blanchet
refactoring
2014-06-26, by blanchet
removed experimental machine learning engine
2014-06-26, by blanchet
store string-to-index tables in memory
2014-06-26, by blanchet
disable 'extra' feature tainting for now
2014-06-26, by blanchet
tuning
2014-06-26, by blanchet
tuning
2014-06-26, by blanchet
tuning
2014-06-26, by blanchet
tuning
2014-06-26, by blanchet
tuning
2014-06-26, by blanchet
honor visible in SML naive Bayes
2014-06-26, by blanchet
honor visibility in SML k-NN
2014-06-26, by blanchet
got rid of a few experimental options
2014-06-26, by blanchet
tuning
2014-06-26, by blanchet
killed dead code
2014-06-26, by blanchet
avoid subscripting array with ~1
2014-06-26, by blanchet
killed dead data
2014-06-26, by blanchet
new version of adaptive k-NN with TFIDF
2014-06-26, by blanchet
refactoring
2014-06-26, by blanchet
tuning
2014-06-26, by blanchet
refactoring
2014-06-26, by blanchet
adaptive k-NN
2014-06-26, by blanchet
avoid parallelism, since it confuses the global state and leads to cheating (with 'sml_xxx' engines)
2014-06-26, by blanchet
generate right dependencies in MaSh driver
2014-06-26, by blanchet
more on "Futures";
2014-06-23, by wenzelm
more on "Futures";
2014-06-23, by wenzelm
more on "Future values";
2014-06-21, by wenzelm
more on "Lazy evaluation";
2014-06-21, by wenzelm
more on syntax phases;
2014-06-20, by wenzelm
more on syntax phases;
2014-06-19, by wenzelm
tuned;
2014-06-19, by wenzelm
tuned;
2014-06-19, by wenzelm
tuned;
2014-06-19, by wenzelm
tuned;
2014-06-19, by wenzelm
tuned;
2014-06-19, by wenzelm
added screenshot;
2014-06-18, by wenzelm
tuned;
2014-06-18, by wenzelm
misc tuning;
2014-06-18, by wenzelm
added screenshot;
2014-06-17, by wenzelm
misc tuning;
2014-06-17, by wenzelm
formal check of jEdit actions;
2014-06-16, by wenzelm
more on "Completion";
2014-06-16, by wenzelm
more on "Completion";
2014-06-16, by wenzelm
tuned;
2014-06-16, by wenzelm
clarified role of old user interfaces as misc tools;
2014-06-16, by wenzelm
added Index;
2014-06-16, by wenzelm
more on "Completion";
2014-06-14, by wenzelm
more on "Completion";
2014-06-13, by wenzelm
tuned;
2014-06-13, by wenzelm
more on "Completion";
2014-06-13, by wenzelm
more on "Completion";
2014-06-12, by wenzelm
more on "Auxiliary files";
2014-06-11, by wenzelm
more on "Document model";
2014-06-11, by wenzelm
suppress index;
2014-06-09, by wenzelm
more on command-line invocation -- moved material from system manual;
2014-06-09, by wenzelm
clarified section structure;
2014-06-09, by wenzelm
clarified section structure;
2014-06-09, by wenzelm
clarified section structure;
2014-06-09, by wenzelm
more on dockable windows;
2014-06-09, by wenzelm
clarified section structure;
2014-06-09, by wenzelm
tuned;
2014-06-06, by wenzelm
more on Query panel;
2014-06-06, by wenzelm
updated screenshots;
2014-06-06, by wenzelm
more on Query panel -- updated Find Theorems;
2014-06-05, by wenzelm
misc tuning and updates;
2014-06-04, by wenzelm
merged
2014-06-25, by Andreas Lochbihler
add lemma
2014-06-24, by Andreas Lochbihler
tuning
2014-06-24, by blanchet
optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
2014-06-24, by blanchet
minor table access optimization
2014-06-24, by blanchet
document property 'rel_coinduct'
2014-06-24, by desharna
tune the implementation of 'rel_coinduct'
2014-06-24, by desharna
generate 'rel_coinduct' theorem for codatatypes
2014-06-24, by desharna
generate 'rel_coinduct0' theorem for codatatypes
2014-06-24, by desharna
added parentheses around type arguments in THF
2014-06-24, by blanchet
optimize log
2014-06-24, by blanchet
enable TF-IDF
2014-06-24, by blanchet
added another experimental engine
2014-06-24, by blanchet
tweaked experimental setup
2014-06-24, by blanchet
changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
2014-06-24, by blanchet
use strings to communicate with external process, to ease debugging
2014-06-24, by blanchet
added 'dummy_thf_ml' prover for experiments with HOLyHammer
2014-06-24, by blanchet
phantoms may also occur in THF1
2014-06-24, by blanchet
added experimental MaSh engine
2014-06-24, by blanchet
move method silencing code closer to the methods it is trying to silence, to reduce bad side-effects
2014-06-24, by blanchet
help reconstruction of Z3 skolemization by weakening formulas a bit
2014-06-24, by blanchet
supports gradual skolemization (cf. Z3) by threading context through correctly
2014-06-24, by blanchet
given two one-liners, only show the best of the two
2014-06-24, by blanchet
don't generate Isar proof skeleton for what amounts to a one-line proof
2014-06-24, by blanchet
don't accidentally transform 'show' into 'obtains' (in general, more 'obtain's could be turned into 'have's, but this is not necessary for the correctness of the proof)
2014-06-24, by blanchet
r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
2014-06-22, by nipkow
added [simp]
2014-06-21, by nipkow
Two basic lemmas on bij_betw.
2014-06-21, by ballarin
changed default MaSh parameters based on (in vitro) evaluation
2014-06-20, by blanchet
made 'tptp_graph' more liberal (why reject TFF?)
2014-06-20, by blanchet
made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
2014-06-18, by blanchet
more MaSh engine variations, for evaluations
2014-06-18, by blanchet
split parameter into two
2014-06-18, by blanchet
filters are easier to define with INF on filters.
2014-06-18, by hoelzl
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
2014-06-18, by hoelzl
more generous formula -- there are lots of duplicates out there
2014-06-18, by blanchet
automatically learn MaSh facts also in 'blocking' mode
2014-06-18, by blanchet
enabled MaSh by default -- set 'MaSh' to 'none' in Isabelle Plugin Options to disable
2014-06-18, by blanchet
Lemmas contributed by Joachim Breitner.
2014-06-17, by ballarin
reintroduce atomize in Waldmeister code
2014-06-17, by blanchet
changed type encoding for new Waldmeister, to trigger filtering of 'dangerous' lemmas
2014-06-17, by blanchet
compile
2014-06-16, by blanchet
integrated new Waldmeister code with 'sledgehammer' command
2014-06-16, by blanchet
fixed parsing of one-argument 'file()' in TSTP files
2014-06-16, by blanchet
use right delimiters for Waldmeister proofs
2014-06-16, by blanchet
added 'waldmeister_new' as ATP
2014-06-16, by blanchet
simplified code
2014-06-16, by blanchet
moved code around
2014-06-16, by blanchet
give Z3 TPTP proofs a chance
2014-06-16, by blanchet
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
2014-06-16, by blanchet
add more derivative and continuity rules for complex-values functions
2014-06-16, by hoelzl
Moving the remote prefix deleting on Sledgehammer's side
2014-06-16, by fleury
Correcting the type parser
2014-06-16, by fleury
imported patch leo2_skolem_simplication
2014-06-16, by fleury
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
2014-06-16, by fleury
lemmas about the moments of the normal distribution
2014-06-16, by hoelzl
NEWS
2014-06-13, by paulson
properties of normal distributed random variables (by Sudeep Kanav)
2014-06-13, by hoelzl
announce Tree
2014-06-13, by nipkow
new theory of binary trees
2014-06-12, by nipkow
formal variable name: IVar NONE is strictly spoken not supported on lhs of function definitions, e.g. in Scala
2014-06-12, by haftmann
merged
2014-06-12, by nipkow
added [simp]
2014-06-12, by nipkow
tuning
2014-06-12, by blanchet
renamed Sledgehammer options
2014-06-12, by blanchet
removed dead code
2014-06-12, by blanchet
reintroduced vital 'Thm.transfer'
2014-06-12, by blanchet
tuned dependencies
2014-06-12, by blanchet
updated docs
2014-06-12, by blanchet
added support for CVC4 in SMT2
2014-06-12, by blanchet
don't ask proof-disabled solvers to do proofs
2014-06-12, by blanchet
tuning
2014-06-12, by blanchet
took out broken support for Yices from SMT2 stack -- see 'NEWS' for rationale
2014-06-12, by blanchet
made CVC3 work with SMT2 stack
2014-06-12, by blanchet
properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
2014-06-12, by hoelzl
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
2014-06-11, by hoelzl
uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor
2014-06-12, by haftmann
adapted examples to changes in SMT triggers
2014-06-12, by blanchet
reduces Sledgehammer dependencies
2014-06-12, by blanchet
eliminate dependency of SMT2 module on 'list'
2014-06-12, by blanchet
tuning
2014-06-12, by blanchet
removed subsumed record-related code, now that records are registered as 'ctr_sugar'
2014-06-12, by blanchet
made lookup more robust in the face of missing (dummy) case constant
2014-06-12, by blanchet
use 'ctr_sugar' abstraction in SMT(2)
2014-06-12, by blanchet
register record extensions as freely generated types
2014-06-12, by blanchet
mixin definitions are within scope of "for"s of import expression
2014-06-11, by haftmann
proper proof context transfer wrt. background theory avoids ad-hoc restore operation
2014-06-11, by haftmann
refactoring
2014-06-11, by blanchet
moved generic code further up
2014-06-11, by blanchet
tuned code
2014-06-11, by blanchet
factor out SMT-LIB 2 type/term parsing from Z3-specific code
2014-06-11, by blanchet
simplify slightly ATP proof generated for Z3
2014-06-11, by blanchet
tuned whitespaces
2014-06-11, by steckerm
updated contributors to include students
2014-06-11, by blanchet
moved new highly experimental Waldmeister-specific code (authored by Albert Steckermeier) into Isabelle
2014-06-11, by blanchet
adapted SMT examples to new, corrected handling of 'typedef'
2014-06-11, by blanchet
fixed unsoundness in SMT(2) as oracle: don't register typedef Abs_x as constructor unless it is known to be injective
2014-06-11, by blanchet
updated NEWS slightly
2014-06-11, by blanchet
updated docs w.r.t. Z3
2014-06-11, by blanchet
rationalized CVC3 and Yices environment variable -- no need (unlike for Z3) to distinguish between old and new versions
2014-06-11, by blanchet
removed '_new' sufffix in SMT2 solver names (in some cases)
2014-06-11, by blanchet
removed old SMT module from Sledgehammer
2014-06-11, by blanchet
got rid of 'listF' example, which is now subsumed by the real 'list' type
2014-06-11, by blanchet
changed syntax of map: and rel: arguments to BNF-based datatypes
2014-06-10, by blanchet
tuning
2014-06-10, by blanchet
updated Z3 certificates
2014-06-10, by blanchet
generate ':named' attributes in SMT-LIB 2 problems, to facilitate reconstruction
2014-06-10, by blanchet
tuning
2014-06-10, by blanchet
add type class instances for unit
2014-06-10, by Andreas Lochbihler
use 'where' clause for selector default value syntax
2014-06-10, by blanchet
tuning
2014-06-10, by blanchet
added List.union
2014-06-09, by nipkow
Sup/Inf on functions decoupled from complete_lattice.
2014-06-09, by nipkow
tuned data structure
2014-06-08, by haftmann
recovered level-free fishing for locale, accidentally lost in dce365931721
2014-06-08, by haftmann
tuned terminology: emphasize stack-like nature of nested local theories
2014-06-08, by haftmann
self-contained locale_declaration operation
2014-06-08, by haftmann
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
2014-06-08, by haftmann
tuned
2014-06-08, by haftmann
recovered structure of module, which got somehow convoluted due to incremental modifications
2014-06-08, by haftmann
re-unified approach towards class and locale consts, with refined terminology: foo_const_declaration denotes declaration for a particular logical layer, foo_const the full stack for a particular target
2014-06-08, by haftmann
revert effect of 63c7b29d29ac -- existing pervasive interpretation of class order for dvd etc. is too obstrusive at the moment
2014-06-08, by haftmann
less ad-hoc verision of educated guess: guess identity of declaration morphism wrt. canonical morphism rather than observing particular effects of declaration morphisms only;
2014-06-08, by haftmann
treat non-canonical interpretations of classes the same way as ordinary locale interpretations
2014-06-07, by haftmann
tuned
2014-06-07, by haftmann
avoid odd Named_Target.reinit altogether
2014-06-07, by haftmann
clarified terminology: toplevel is interwined with named targets in particular, not with local theories in general
2014-06-07, by haftmann
less baroque interface
2014-06-07, by haftmann
less
more
|
(0)
-30000
-10000
-3000
-1000
-960
+960
+1000
+3000
+10000
tip