isabelle: Graph

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
dropped obscure and unused ad-hoc before_exit hook for named targets
2014-06-06, by haftmann
added lemma
2014-06-06, by nipkow
mira: USER_HOME must exist for building JEdit documentation
2014-06-05, by noschinl
added lemmas
2014-06-06, by nipkow
sharpened criterion: bare named target is only at the bottom level
2014-06-05, by haftmann
tuned
2014-06-05, by haftmann
extended stream library
2014-06-05, by traytel
be more explicit: made sml/nj happy
2014-06-05, by haftmann
always refine interpretation morphism using canonical constant's definition theorem
2014-06-05, by haftmann
set USER_HOME to affect also ISABELLE_PATH et al
2014-06-04, by noschinl
merge
2014-06-03, by blanchet
updated SMT2 certificates
2014-06-03, by blanchet
tune
2014-06-03, by blanchet
disable hard-to-reconstruct Z3 feature
2014-06-03, by blanchet
new Z3 4.3.2 component, based on more recent repository version, and whose Mac binary was built on Mac OS X 10.7
2014-06-03, by blanchet
use 0 as integral-value for non-integrable functions, simplify a couple of rewrite rules
2014-06-03, by hoelzl
removed SMT weights -- their impact was very inconclusive anyway
2014-06-03, by blanchet
make SMT code less dependent on Z3 proofs
2014-06-03, by blanchet
tuning
2014-06-03, by blanchet
avoid division by 0
2014-06-02, by blanchet
formal treatment of dangling parameters for class abbrevs analogously to class consts
2014-06-02, by haftmann
explicit passing of params
2014-06-02, by haftmann
refactored Z3 to Isar proof construction code
2014-06-02, by blanchet
simplified counterexample handling
2014-06-02, by blanchet
split replay and proof parsing for Z3
2014-06-02, by blanchet
removed counterexample parser (obsolete and useless in practice)
2014-06-02, by blanchet
remove superfluous assumption
2014-06-02, by hoelzl
basic setup for zipperposition prover
2014-06-02, by fleury
document property 'sel_set'
2014-06-02, by desharna
generate 'sel_set' theorem for (co)datatypes
2014-06-02, by desharna
removed some spurious warnings in new (co)datatype package
2014-06-02, by blanchet
add option to keep duplicates, for more precise evaluation of relevance filters
2014-06-02, by blanchet
tuned whitespace
2014-06-02, by blanchet
definition in class: provide explicit auxiliary abbreviation carrying potential mixfix syntax in presence of dangling parameters
2014-06-01, by haftmann
tuned
2014-06-01, by haftmann
merged
2014-05-31, by boehmes
tuned
2014-05-31, by boehmes
more complete proof replay for Z3: support universally quantified rewrite steps
2014-05-31, by boehmes
postpone const declarations for nested context after canonical const declarations: keep const declarations stemming from interpretation together
2014-05-31, by haftmann
tuned
2014-05-31, by haftmann
explicit is better than implicit
2014-05-31, by haftmann
tuned names
2014-05-31, by haftmann
dropped accidental duplicate application of morphism
2014-05-31, by haftmann
generalizd measurability on restricted space; rule for integrability on compact sets
2014-05-30, by hoelzl
better support for restrict_space
2014-05-30, by hoelzl
must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
2014-05-30, by nipkow
merged
2014-05-30, by wenzelm
updated cygwin -- include perl_vendor for libwww-perl;
2014-05-30, by wenzelm
made 'Kuehlwein-style' be really like Python code, we now think
2014-05-30, by blanchet
make SML code closer to Python code when 'nb_kuehlwein_style' is true
2014-05-30, by blanchet
merge
2014-05-30, by blanchet
added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away
2014-05-30, by blanchet
introduce more powerful reindexing rules for big operators
2014-05-30, by hoelzl
merged
2014-05-30, by wenzelm
make double-sure that old popup is dismissed, before replacing it;
2014-05-30, by wenzelm
more robust bold_style, e.g. relevant for accidental \<^bold> before keyword;
2014-05-30, by wenzelm
added another way of invoking Python code, for experiments
2014-05-30, by blanchet
make SML naive Bayes closer to Python version
2014-05-30, by blanchet
tuned whitespace, to make datatype definitions slightly less intimidating
2014-05-30, by blanchet
more work on exporter
2014-05-30, by blanchet
got rid of 'linearize' option
2014-05-30, by blanchet
extend exporter with new versions of MaSh
2014-05-30, by blanchet
tuned
2014-05-30, by haftmann
tuned signature
2014-05-30, by haftmann
terminating code equations
2014-05-30, by haftmann
more direct passing of right-hand side
2014-05-29, by haftmann
even more uniform treatment of result after 95e5a633a18f
2014-05-29, by haftmann
Merge
2014-05-29, by paulson
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
2014-05-29, by paulson
removed Kleene_Algebra because of superior AFP entry; authors agreed
2014-05-29, by nipkow
typo
2014-05-29, by nipkow
uniform treatmen of result
2014-05-28, by haftmann
tuned variable names
2014-05-28, by haftmann
more generous max number of suggestions, for more safety
2014-05-28, by blanchet
changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)
2014-05-28, by blanchet
export more ML functions, for experimentation
2014-05-28, by blanchet
tuned signature;
2014-05-28, by wenzelm
disabled IDF for now -- empirical evidence points the wrong way (as usual)
2014-05-28, by blanchet
tuning
2014-05-28, by blanchet
tuning
2014-05-28, by blanchet
optimized computation
2014-05-28, by blanchet
enabled IDF for naive Bayes ML
2014-05-28, by blanchet
tuning
2014-05-28, by blanchet
repaired subscript problem in SML kNN
2014-05-28, by blanchet
tuning
2014-05-28, by blanchet
always remove duplicates in meshing + use weights for Naive Bayes
2014-05-28, by blanchet
updated naive Bayes
2014-05-27, by blanchet
don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
2014-05-27, by blanchet
don't conceal (co)datatypes
2014-05-26, by blanchet
changed '-:' to 'dead' in BNF
2014-05-26, by blanchet
got rid of '=:' squiggly
2014-05-26, by blanchet
use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax
2014-05-26, by blanchet
renamed 'MaSh' option
2014-05-26, by blanchet
document '=:' syntax better
2014-05-26, by blanchet
capitalize even more carefully (see 5ac67041ccf8), e.g. relevant for option "z3_non_commercial" and prospective "MaSh";
2014-05-26, by wenzelm
tuned;
2014-05-25, by wenzelm
clarified copy_file: allow to rename base name, e.g. relevant for 'display_drafts';
2014-05-24, by wenzelm
support for regular Windows TeX installation;
2014-05-24, by wenzelm
more portable file names;
2014-05-24, by wenzelm
more portable -- accomodate MiKTeX on Windows;
2014-05-24, by wenzelm
receovered alternative abbrevs for \<open> \<close> from 8e8243975860, to accommodate national keyboard layouts where "`" might be hard to produce;
2014-05-24, by wenzelm
strip trailing white space, to avoid notorious problems of jEdit with last line;
2014-05-24, by wenzelm
added fifth member to BNF team
2014-05-23, by blanchet
removed noise
2014-05-23, by blanchet
fixed semantics of 'linearize'
2014-05-23, by blanchet
automatically reload state file when it changes on disk
2014-05-23, by blanchet
tuned
2014-05-22, by haftmann
tuned names
2014-05-22, by haftmann
tuned signature
2014-05-22, by haftmann
moved const declaration further down in bootstrap hierarchy: keep Named_Target free of low-level stuff
2014-05-22, by haftmann
unused
2014-05-22, by haftmann
tuned
2014-05-22, by haftmann
more uniform order of operations;
2014-05-22, by haftmann
common background_abbrev operation
2014-05-22, by haftmann
tuned signature
2014-05-22, by haftmann
tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
2014-05-22, by haftmann
compactified
2014-05-22, by haftmann
include Nominal2 keywords -- Proof General legacy;
2014-05-22, by wenzelm
another attempt to revive isatest -- reverting 801c01004a21;
2014-05-22, by wenzelm
avoid slow inspection of proof terms now that dependencies are stored in 'state'
2014-05-22, by blanchet
properly mark relearns as dirty
2014-05-22, by blanchet
disable weights that cause more harm than they help in kNN
2014-05-22, by blanchet
add self dependency to naive Bayes
2014-05-22, by blanchet
make MaSh Python the default when passing 'fact_filter = mash' without enabling the 'maSh' Isabelle system option
2014-05-22, by blanchet
compactified level discriminator
2014-05-22, by haftmann
properly reconstruct helpers in Z3 proofs
2014-05-22, by blanchet
reverted '|' features in MaSh -- these sounded like a good idea but never really worked
2014-05-22, by blanchet
tuning
2014-05-22, by blanchet
shorten Sledgehammer output, as suggested by Andrei Popescu
2014-05-22, by blanchet
until naive Bayes supports weights, don't incorporate 'extra' low-weight features
2014-05-22, by blanchet
spell-checker completion is restricted to explicit mode, to avoid odd effects with immediate edits vs. delayed language context markup, and occasional delays due to dictionary lookup of many variants;
2014-05-21, by wenzelm
merged
2014-05-21, by wenzelm
updated to scala-2.11.1, with full uncensored classpath;
2014-05-21, by wenzelm
updated cygwin more thoroughly;
2014-05-21, by wenzelm
document property 'sel_map'
2014-05-21, by desharna
generate 'sel_map[simp]' theorem for (co)datatypes and tuning 'disc_map_iff'
2014-05-21, by desharna
merged
2014-05-21, by wenzelm
more uniform Font_Info.Zoom_Box;
2014-05-21, by wenzelm
added zoom box, like for outer output windows;
2014-05-21, by wenzelm
tuned signature;
2014-05-21, by wenzelm
consolidate "break_thm" and "break_term" attributes into "simp_break";
2014-05-21, by Lars Hupel
docs
2014-05-21, by blanchet
added comment
2014-05-21, by blanchet
move exhaust first, for technical reasons
2014-05-21, by blanchet
avoid markup-generating @{make_string}
2014-05-21, by blanchet
generalized Bochner integral over infinite sums
2014-05-21, by hoelzl
unused;
2014-05-21, by wenzelm
obsolete;
2014-05-21, by wenzelm
approximative update of versions;
2014-05-21, by wenzelm
incorporate isabelle.graphview into Pure.jar, which saves 20..30s build time;
2014-05-21, by wenzelm
remove stray println;
2014-05-21, by Lars Hupel
CONTRIBUTORS
2014-05-20, by blanchet
added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)
2014-05-20, by blanchet
added Isabelle system option 'mash'
2014-05-20, by blanchet
updated cygwin;
2014-05-20, by wenzelm
afford strict check (see also AFP/a8e08d947f0a);
2014-05-20, by wenzelm
add various lemmas
2014-05-20, by hoelzl
merged
2014-05-20, by wenzelm
merged
2014-05-20, by wenzelm
adhoc move to lxbroy10, which has 120 GB more memory than lxbroy2;
2014-05-20, by wenzelm
explicit treatment of unfinished cartouches, which is important for Thy_Syntax.consolidate_spans;
2014-05-20, by wenzelm
news
2014-05-20, by blanchet
updated docs
2014-05-20, by blanchet
more flexible environment variable
2014-05-20, by blanchet
tuning
2014-05-20, by blanchet
added unit :: linorder
2014-05-20, by nipkow
added lemma
2014-05-20, by nipkow
implemented MaSh/SML hints
2014-05-20, by blanchet
better way to take invisible facts into account than 'island' business
2014-05-20, by blanchet
cleaner handling of learned proofs
2014-05-20, by blanchet
implemented learning of single proofs in SML MaSh
2014-05-20, by blanchet
take weights into consideration in knn
2014-05-19, by blanchet
added SML implementation of MaSh
2014-05-19, by blanchet
use E 1.8's auto scheduler option
2014-05-19, by blanchet
started work on MaSh/SML
2014-05-19, by blanchet
tune
2014-05-19, by blanchet
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
2014-05-19, by blanchet
trace windows uses search feature of Pretty_Text_Area;
2014-05-19, by Lars Hupel
obsolete -- always pdf;
2014-05-19, by wenzelm
prefer T1 with searchable underscore (requires proper cm-super fonts);
2014-05-19, by wenzelm
merged
2014-05-19, by wenzelm
some adhoc event handling to unify L&F button focus behavior, e.g. Mac OS X vs. Nimbus;
2014-05-19, by wenzelm
re-focus target explicity, e.g. relevant for Sledgehammer panel;
2014-05-19, by wenzelm
clarified is_text in accordance to ML version (7e0178c84994), e.g. relevant for 'header' syntax in PIDE front-end;
2014-05-19, by wenzelm
more explicit identification for more robust adhoc change of environment /home/isatest/.isabelle/etc/settings -- notably for $ISABELLE_PLATFORM64;
2014-05-19, by wenzelm
renamed positive_integral to nn_integral
2014-05-19, by hoelzl
hide more consts to beautify documentation
2014-05-19, by blanchet
fixed document generation for HOL-Probability
2014-05-19, by hoelzl
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
2014-05-19, by hoelzl
document property 'disc_map_iff'
2014-05-19, by desharna
generate 'disc_map_iff[simp]' theorem for (co)datatypes
2014-05-15, by desharna
fix 'set_empty' theorem when the discriminator is 'op ='
2014-05-19, by desharna
typos
2014-05-18, by nipkow
tuned comments;
2014-05-18, by wenzelm
clarified dependencies -- Mavericks presently does not work;
2014-05-18, by wenzelm
clarified docking layout, amending 9c2ca698690e;
2014-05-18, by wenzelm
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
2014-05-16, by blanchet
removed needless transfer
2014-05-16, by blanchet
use 'simp add:' syntax in Sledgehammer rather than 'using'
2014-05-16, by blanchet
silence methods even better
2014-05-16, by blanchet
honor original format of conjecture or hypotheses in Z3-to-Isar proofs
2014-05-16, by blanchet
proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;
2014-05-16, by wenzelm
added lemmas for -1
2014-05-16, by noschinl
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')
2014-05-16, by blanchet
new syntax for card, normalized spacing for #
2014-05-16, by nipkow
clarified stylized status of sandwich algebra
2014-05-15, by haftmann
dropped dead code
2014-05-15, by haftmann
accurate separation of static and dynamic context
2014-05-15, by haftmann
syntactic means to prevent accidental mixup of static and dynamic context
2014-05-15, by haftmann
proper separation of static and dynamic context
2014-05-15, by haftmann
optimization for trivial cases
2014-05-15, by haftmann
modernized setup
2014-05-15, by haftmann
dropped obsolete hand-waving adjustion of type variables: safely done in preprocessor
2014-05-15, by haftmann
unified approach toward conversions and simple term rewriting in preprocessor by means of sandwiches
2014-05-15, by haftmann
normalize type variables of evaluation term by conversion
2014-05-15, by haftmann
more aggressive nested size handling in the absence of 'size_o_map' theorems (+ unrelated pattern matching fix)
2014-05-15, by blanchet
new approach to silence proof methods, to avoid weird theory/context mismatches
2014-05-15, by blanchet
type
2014-05-15, by haftmann
merged
2014-05-14, by wenzelm
restrict default docking layout to bare minimum -- NB: Simplifier Trace still needs fine-tuning to show up on demand;
2014-05-14, by wenzelm
updated isatest;
2014-05-14, by wenzelm
updated to polyml-5.5.2;
2014-05-14, by wenzelm
practically obsolete: plain "poly" should work, except for Linux without libgmp installed;
2014-05-14, by wenzelm
updated to polyml-5.5.2;
2014-05-14, by wenzelm
document 'set_empty'
2014-05-14, by desharna
generate 'set_empty' theorem for BNFs
2014-05-12, by desharna
document 'map_id0'
2014-05-08, by desharna
note map_id0 more often
2014-05-08, by desharna
added lemma
2014-05-14, by nipkow
added lemmas
2014-05-13, by nipkow
transfer theorems since 'silence_methods' may change the theory
2014-05-13, by blanchet
add mono rules for diff
2014-05-13, by hoelzl
clean up Lebesgue integration
2014-05-13, by hoelzl
more bnf_decl -> bnf_axiomatization
2014-05-13, by blanchet
tuned docs
2014-05-13, by blanchet
hide more internal names
2014-05-13, by blanchet
tuning
2014-05-13, by blanchet
no reset for 'end' -- e.g. relevant for 'notepad';
2014-05-13, by wenzelm
updated keywords
2014-05-13, by traytel
bnf_decl -> bnf_axiomatization
2014-05-13, by traytel
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
2014-05-12, by wenzelm
Replaced refute with nitpick.
2014-05-12, by webertj
NEWS;
2014-05-12, by wenzelm
tuned message;
2014-05-12, by wenzelm
smarter recovery from toplevel type error;
2014-05-12, by wenzelm
more direct patch of public interface DockableWindowContainer -- avoid package org.gjt.sp.jedit.gui intrusion;
2014-05-11, by wenzelm
updated keywords;
2014-05-09, by wenzelm
merged
2014-05-09, by wenzelm
more markup;
2014-05-09, by wenzelm
more position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-09, by wenzelm
always bounce focus back to main text area, unless explicit focus component is given here (see also 7b65f4da136d);
2014-05-09, by wenzelm
tuned signature;
2014-05-09, by wenzelm
delete attribute for code abbrev
2014-05-09, by haftmann
dropped term_of obfuscation -- not really required;
2014-05-09, by haftmann
hardcoded nbe and sml into value command
2014-05-09, by haftmann
modernized setups
2014-05-09, by haftmann
degeneralized value command into HOL
2014-05-09, by haftmann
dimiss simplified as evaluator due to little practical relevance
2014-05-09, by haftmann
prefer separate command for approximation
2014-05-09, by haftmann
removed junk from library theory
2014-05-09, by haftmann
note of_class rule for type classes in theory: useful to promote class instance proofs to locale interpretation proofs
2014-05-09, by haftmann
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
2014-05-09, by haftmann
tuned GUI;
2014-05-08, by wenzelm
clarified detach_operation: ignore empty output;
2014-05-08, by wenzelm
bounce focus back to main text area -- Output is for output, not query input;
2014-05-08, by wenzelm
update for release;
2014-05-08, by wenzelm
merged
2014-05-08, by wenzelm
tuned message;
2014-05-08, by wenzelm
no qualifier for now, to avoid confusion concerning loaded_theories in PIDE interaction;
2014-05-08, by wenzelm
some position markup to help locating the query context, e.g. from "Info" dockable;
2014-05-08, by wenzelm
tuned GUI;
2014-05-08, by wenzelm
tuned GUI;
2014-05-08, by wenzelm
tuned GUI;
2014-05-08, by wenzelm
tuned message: more compact, imitate actual command line;
2014-05-08, by wenzelm
enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
2014-05-08, by wenzelm
some odd tricks to provide "Detach" menu item, via "PIDE" docking framework;
2014-05-08, by wenzelm
untyped, unscoped, unchecked access to JVM objects;
2014-05-08, by wenzelm
Documented new property
2014-05-08, by desharna
generate 'map_ident' theorem for BNFs
2014-05-08, by desharna
explicit option to build library, which takes most of the time;
2014-05-07, by wenzelm
NEWS;
2014-05-07, by wenzelm
merged
2014-05-07, by wenzelm
more symbols;
2014-05-07, by wenzelm
tuned message: "step" goes back to TTY mode before Proof General, while "depth" is more informative but sometimes confusing due to implementation details;
2014-05-07, by wenzelm
print results as "state", to avoid intrusion into the source text;
2014-05-07, by wenzelm
run commands as interactive, again after long history of fluctuation (9e196062bf88, 173974e07dea, e07dacec79e7) and quite different infrastructure for print tasks;
2014-05-07, by wenzelm
discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
2014-05-07, by wenzelm
more emphatic output for Proof General;
2014-05-07, by wenzelm
tuned;
2014-05-07, by wenzelm
tuned defaults;
2014-05-07, by wenzelm
tuned message -- more context for detached window etc.;
2014-05-07, by wenzelm
tuned signature;
2014-05-07, by wenzelm
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
2014-05-07, by hoelzl
tuned GUI for Windows L&F;
2014-05-06, by wenzelm
clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
2014-05-06, by wenzelm
tuned GUI layout;
2014-05-06, by wenzelm
clarified GUI events, e.g. relevant for insert via completion;
2014-05-06, by wenzelm
more robust line_range, according to usual jEdit confusion at end of last line (see also 71c5d1f516c0);
2014-05-06, by wenzelm
common support for search field, which is actually a light-weight Highlighter;
2014-05-06, by wenzelm
clarified GUI focus;
2014-05-06, by wenzelm
more uniform detach button;
2014-05-06, by wenzelm
tuned signature;
2014-05-06, by wenzelm
renamed "Find" to "Query", with more general operations;
2014-05-06, by wenzelm
hardwired default_frequency to avoid fluctuation of popup content;
2014-05-06, by wenzelm
more visual feedback on path_completion, at the risk of file-system access in GUI painting;
2014-05-06, by wenzelm
tuned;
2014-05-06, by wenzelm
explicit option parallel_print to downgrade parallel scheduling, which might occasionally help for big and heavy "scripts";
2014-05-06, by wenzelm
tuned GUI layout;
2014-05-06, by wenzelm
tuned;
2014-05-06, by wenzelm
some complication with ListView.Renderer to get tooltips;
2014-05-05, by wenzelm
expose interrupts more like ML version, but not in managed bash processes of Build;
2014-05-05, by wenzelm
merged
2014-05-05, by wenzelm
uniform Toplevel.print for all proof commands;
2014-05-05, by wenzelm
clarified print operations for "terms" and "theorems";
2014-05-05, by wenzelm
more print operations;
2014-05-05, by wenzelm