isabelle: Graph

merged
2011-07-06, by wenzelm
make SML/NJ happier
2011-07-06, by blanchet
make SML/NJ happy + tuning
2011-07-06, by blanchet
moved ATP dependencies to HOL-Plain, where they belong
2011-07-06, by blanchet
better setup for experimental "z3_atp"
2011-07-06, by blanchet
64bit versions of some mira configurations
2011-07-06, by krauss
removed unused mira configuration
2011-07-06, by krauss
merged
2011-07-06, by bulwahn
tuning options to avoid spurious isabelle test failures
2011-07-06, by bulwahn
clarified record syntax: fieldext excludes the "more" pseudo-field (unlike 2f885b7e5ba7), so that errors like (| x = a, more = b |) are reported less confusingly;
2011-07-06, by wenzelm
prefer Synchronized.var;
2011-07-06, by wenzelm
tuned errors;
2011-07-06, by wenzelm
record package: proper configuration options;
2011-07-06, by wenzelm
just one copy of split_args;
2011-07-06, by wenzelm
merged
2011-07-06, by wenzelm
rename lemma Infinite_Product_Measure.sigma_sets_subseteq, it hides Sigma_Algebra.sigma_sets_subseteq
2011-07-05, by hoelzl
improved translation of lambdas in THF
2011-07-05, by nik
added generation of lambdas in THF
2011-07-05, by nik
add support for lambdas in TPTP THF generator + killed an unsound type encoding (because the monotonicity calculus assumes first-order)
2011-07-05, by nik
simplified Symbol.iterator: produce strings, which are mostly preallocated;
2011-07-05, by wenzelm
tuned comment (cf. e9f26e66692d);
2011-07-05, by wenzelm
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
2011-07-05, by wenzelm
theory name needs to conform to Path syntax;
2011-07-05, by wenzelm
hard-wired print mode "xsymbols" increases chance that "iff" in HOL will print symbolic arrow;
2011-07-05, by wenzelm
prefer space_explode/split_lines as in Isabelle/ML;
2011-07-05, by wenzelm
Path.split convenience;
2011-07-05, by wenzelm
get theory from last executation state;
2011-07-05, by wenzelm
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
2011-07-05, by wenzelm
clarified cancel_execution/await_cancellation;
2011-07-05, by wenzelm
tuned signature;
2011-07-05, by wenzelm
tuned;
2011-07-05, by wenzelm
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
2011-07-05, by krauss
Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);
2011-07-04, by wenzelm
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
2011-07-04, by wenzelm
explicit class Counter;
2011-07-04, by wenzelm
merged
2011-07-04, by wenzelm
the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})
2011-07-04, by hoelzl
equalities of subsets of atLeastLessThan
2011-07-04, by hoelzl
adding documentation of the value antiquotation to the code generation manual
2011-07-03, by bulwahn
make SML/NJ happy
2011-07-03, by blanchet
install case certificate for If after code_datatype declaration for bool
2011-07-02, by haftmann
tuned typo
2011-07-02, by haftmann
pervasive Basic_Library in Scala;
2011-07-04, by wenzelm
some support for theory files within Isabelle/Scala session;
2011-07-04, by wenzelm
imitate exception ERROR of Isabelle/ML;
2011-07-04, by wenzelm
eliminated null;
2011-07-03, by wenzelm
more explicit edit_node vs. init_node;
2011-07-03, by wenzelm
tuned signature;
2011-07-03, by wenzelm
Thy_Header.read convenience;
2011-07-02, by wenzelm
some support for Session.File_Store;
2011-07-02, by wenzelm
tuned signature;
2011-07-02, by wenzelm
eliminated redundant session_ready;
2011-07-02, by wenzelm
tuned;
2011-07-02, by wenzelm
uniform finish_thy -- always Global_Theory.join_proofs, even with sequential scheduling;
2011-07-02, by wenzelm
misc tuning;
2011-07-02, by wenzelm
correction: do not assume that case const index covered all cases
2011-07-02, by haftmann
remove illegal case combinators after merge
2011-07-01, by haftmann
corrected misunderstanding what `old functions` are supposed to be
2011-07-01, by haftmann
centralized deletion of equations for constructors; corrected misunderstanding what `old functions` are supposed to be
2011-07-01, by haftmann
merged
2011-07-01, by haftmann
index cases for constructors
2011-07-01, by haftmann
cover induct's "arbitrary" more deeply
2011-07-01, by noschinl
merged;
2011-07-01, by wenzelm
enforce hard timeout on ATPs (esp. "z3_atp" on Linux) + remove obsolete failure codes
2011-07-01, by blanchet
made minimizer informative output accurate
2011-07-01, by blanchet
test a few more type encodings
2011-07-01, by blanchet
further repair "mangled_tags", now that tags are also mangled
2011-07-01, by blanchet
update documentation after "type_enc" renaming + fixed a few other out-of-date factlets
2011-07-01, by blanchet
renamed "type_sys" to "type_enc", which is more accurate
2011-07-01, by blanchet
document "simple_higher" type encoding
2011-07-01, by blanchet
cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
2011-07-01, by blanchet
mangle "ti" tags
2011-07-01, by blanchet
tuning
2011-07-01, by blanchet
clarified Thy_Syntax.element;
2011-07-01, by wenzelm
tuned layout;
2011-07-01, by wenzelm
proper @{binding} antiquotations (relevant for formal references);
2011-07-01, by wenzelm
tuned;
2011-07-01, by wenzelm
merged
2011-07-01, by wenzelm
reverted 782991e4180d: fold_fields was never used
2011-07-01, by noschinl
reverted ce00462f,b3759dce, 7a165592: unwanted generalisation
2011-07-01, by noschinl
improving actual dependencies
2011-07-01, by bulwahn
adding a minimalistic documentation of the value antiquotation in the Isar reference manual
2011-07-01, by bulwahn
adding a value antiquotation
2011-07-01, by bulwahn
more general theory header parsing;
2011-06-30, by wenzelm
back to sequential merge_data, reverting 741373421318 (NB: expensive Parser.merge_gram is already asynchronous since 3daff3cc2214);
2011-06-30, by wenzelm
merged
2011-06-30, by wenzelm
parse term in auxiliary context augmented with variable;
2011-06-30, by krauss
linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
2011-06-29, by boehmes
prefer Isabelle path algebra;
2011-06-30, by wenzelm
proper fold order;
2011-06-30, by wenzelm
more Path operations;
2011-06-30, by wenzelm
getenv_strict in ML;
2011-06-30, by wenzelm
standardized use of Path operations;
2011-06-30, by wenzelm
tuned comments;
2011-06-30, by wenzelm
abstract algebra of file paths in Scala (cf. path.ML);
2011-06-30, by wenzelm
proper Path.print;
2011-06-30, by wenzelm
basic operations on lists and strings;
2011-06-29, by wenzelm
tuned signature;
2011-06-29, by wenzelm
simplified/unified Simplifier.mk_solver;
2011-06-29, by wenzelm
modernized some simproc setup;
2011-06-29, by wenzelm
modernized some simproc setup;
2011-06-29, by wenzelm
print Path.T with some markup;
2011-06-29, by wenzelm
HTML: render control symbols more like Isabelle/Scala/jEdit;
2011-06-29, by wenzelm
collapse map functions with identity subcoercions to identities;
2011-06-28, by traytel
reenabled accidentally-disabled automatic minimization
2011-06-28, by blanchet
tuned markup;
2011-06-28, by wenzelm
merged
2011-06-28, by paulson
tidied messy proofs
2011-06-28, by paulson
merged
2011-06-28, by bulwahn
adding timeout to quickcheck narrowing
2011-06-28, by bulwahn
simplified proofs using metis calls
2011-06-28, by paulson
merged
2011-06-28, by paulson
keyfree: The set of key-free messages (and associated theorems)
2011-06-28, by paulson
merged
2011-06-27, by wenzelm
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor;
2011-06-27, by krauss
added reference for MESON
2011-06-27, by blanchet
document "meson" and "metis" in HOL specific section of the Isar ref manual
2011-06-27, by blanchet
clarify minimizer output
2011-06-27, by blanchet
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
2011-06-27, by blanchet
tweaked comment
2011-06-27, by blanchet
document "sound" option
2011-06-27, by blanchet
minor Sledgehammer news
2011-06-27, by blanchet
added "sound" option to force Sledgehammer to be pedantically sound
2011-06-27, by blanchet
removed "full_types" option from documentation
2011-06-27, by blanchet
document changes to Sledgehammer and "try"
2011-06-27, by blanchet
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
2011-06-27, by blanchet
clarify warning message to avoid confusing beginners
2011-06-27, by blanchet
remove experimental trimming feature -- it slowed down things on Linux for some reason
2011-06-27, by blanchet
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
2011-06-27, by blanchet
NEWS;
2011-06-27, by wenzelm
document antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27, by wenzelm
proper checking of @{ML_antiquotation};
2011-06-27, by wenzelm
hide rather short auxiliary names, which can easily occur in user theories;
2011-06-27, by wenzelm
updated generated file;
2011-06-27, by wenzelm
ML antiquotations are managed as theory data, with proper name space and entity markup;
2011-06-27, by wenzelm
old gensym is now legacy -- global state is out of fashion, and its result is not guaranteed to be fresh;
2011-06-27, by wenzelm
parallel Syntax.parse, which is rather slow;
2011-06-27, by wenzelm
markup binding like class, which is the only special markup where Proof General (including version 4.1) allows "isar-long-id-stuff";
2011-06-27, by wenzelm
move conditional expectation to its own theory file
2011-06-27, by hoelzl
updated SMT certificates
2011-06-26, by boehmes
generalized introduction of explicit application constant: consider more functions as possible witness/instance of quantifiers than before (a constant of type T1 -> T2 -> T3 should be considered to have a rank less or equal to 1 if variables of type T2 -> T3 occur bound in a problem);
2011-06-26, by boehmes
proper tokens only if session is ready;
2011-06-25, by wenzelm
entity markup for "type", "constant";
2011-06-25, by wenzelm
clarified Markup.CLASS vs. HTML.CLASS;
2011-06-25, by wenzelm
tuned color, to avoid confusion with type variables;
2011-06-25, by wenzelm
discontinued generic XML markup -- this is for XHTML with <span/> elements;
2011-06-25, by wenzelm
type classes: entity markup instead of old-style token markup;
2011-06-25, by wenzelm
clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
2011-06-25, by wenzelm
clarified Binding.str_of/print: show full prefix + qualifier, which is relevant for print_locale, for example;
2011-06-25, by wenzelm
produce string constant directly;
2011-06-25, by wenzelm
merged
2011-06-25, by wenzelm
While reading equations of an interpretation, already allow syntax provided by the interpretation base.
2011-06-25, by ballarin
removed very slow proof of unnamed/unused theorem from HOL/Quickcheck_Narrowing.thy (cf. 2dee03f192b7) -- can take seconds for main HOL and minutes for HOL-Proofs;
2011-06-25, by wenzelm
clarified java.ext.dirs: putting Isabelle extensions first makes it work miraculously even on Cygwin with Java in "C:\Program Files\..." (with spaces in file name);
2011-06-25, by wenzelm
CLASSPATH already converted in isabelle java wrapper;
2011-06-25, by wenzelm
removed unused/broken Isabelle.exe for now -- needs update of Admin/launch4j;
2011-06-25, by wenzelm
more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
2011-06-23, by wenzelm
clarified EXCEPTIONS [] (cf. Exn.is_interrupt and Runtime.exn_message);
2011-06-23, by wenzelm
more robust concurrent builds;
2011-06-23, by wenzelm
merged
2011-06-23, by huffman
add countable_datatype method for proving countable class instances
2011-06-23, by huffman
merged;
2011-06-23, by wenzelm
instance inat :: number_semiring
2011-06-23, by huffman
added number_semiring class, plus a few new lemmas;
2011-06-23, by huffman
merged
2011-06-23, by blanchet
fiddle with remote ATP settings, based on Judgment Day
2011-06-23, by blanchet
give slightly more time to server to respond, to avoid leaving too much garbage on Geoff's servers
2011-06-23, by blanchet
Release notes should be written from the user's perspective. Don't assume the user has universal knowledge of the system.
2011-06-23, by ballarin
generalize lemmas power_number_of_even and power_number_of_odd
2011-06-22, by huffman
merged
2011-06-22, by huffman
add HOLCF/ex/Concurrency_Monad.thy, which contains resumption/state/powerdomain monad example from my PhD thesis
2011-06-22, by huffman
simplified arrangement of jars;
2011-06-23, by wenzelm
adapted to Cygwin;
2011-06-23, by wenzelm
provide Isabelle/Scala environment as Java extension, instead of user classpath
2011-06-23, by wenzelm
explicit import java.lang.System to prevent odd scope problems;
2011-06-23, by wenzelm
ensure export of initial CLASSPATH;
2011-06-23, by wenzelm
augment Java extension directories;
2011-06-23, by wenzelm
basic setup for Isabelle charset;
2011-06-23, by wenzelm
prefer actual charset over charset name;
2011-06-22, by wenzelm
clarified default ML settings;
2011-06-22, by wenzelm
lazy Isabelle_System.default supports implicit boot;
2011-06-22, by wenzelm
clarified plugin start/stop;
2011-06-22, by wenzelm
clarified init/exit procedure;
2011-06-22, by wenzelm
clarified decoded control symbols;
2011-06-22, by wenzelm
init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
2011-06-22, by wenzelm
prefer STIXGeneral -- hard to tell if better or worse;
2011-06-22, by wenzelm
merged
2011-06-22, by wenzelm
export lambda-lifting code as there is potential use for it within Sledgehammer
2011-06-22, by boehmes
updated to jedit-4.4.1 and jedit_build-20110622;
2011-06-22, by wenzelm
clarified chunk.offset, chunk.length;
2011-06-22, by wenzelm
avoid fractional font metrics, which makes rendering really ugly (e.g. on Linux);
2011-06-21, by wenzelm
some arrow symbols from DejaVuSansMono for bsub/esub/bsup/esup;
2011-06-21, by wenzelm
more precise font transformations: shift sub/superscript, adjust size for user fonts;
2011-06-21, by wenzelm
don't change the way helpers are generated for the exporter's sake
2011-06-21, by blanchet
provide appropriate type system and number of fact defaults for remote ATPs
2011-06-21, by blanchet
order generated facts topologically
2011-06-21, by blanchet
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
2011-06-21, by blanchet
tweaked E, SPASS, Vampire setup based on latest Judgment Day results
2011-06-21, by blanchet
remove historical bloat -- another benefit of merging Metis's and Sledgehammer's translations
2011-06-21, by blanchet
avoid double ASCII-fication
2011-06-21, by blanchet
make sure that enough type information is generated -- because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
2011-06-21, by blanchet
generate type predicates for existentials/skolems, otherwise some problems might not be provable
2011-06-21, by blanchet
insert rather than append special facts to make it less likely that they're truncated away
2011-06-21, by blanchet
hidden font: full height makes cursor more visible;
2011-06-21, by wenzelm
more uniform treatment of recode_set/recode_map;
2011-06-21, by wenzelm
tuned iteration over short symbols;
2011-06-21, by wenzelm
Symbol.is_ctrl: handle decoded version as well;
2011-06-21, by wenzelm
some support for user symbol fonts;
2011-06-21, by wenzelm
removed obsolete font specification;
2011-06-20, by wenzelm
more tolerant Symbol.decode;
2011-06-20, by wenzelm
simplified/generalized ISABELLE_FONTS handling;
2011-06-20, by wenzelm
updated to jedit_build-20110620;
2011-06-20, by wenzelm
added SyntaxUtilities.StyleExtender hook, with actual functionality in Isabelle/Scala;
2011-06-20, by wenzelm
clean up SPASS FLOTTER hack
2011-06-20, by blanchet
remove automatic recovery from (some) unsound proofs, now that we use sound encodings for all the interesting provers
2011-06-20, by blanchet
only refer to facts found in TPTP file -- e.g. facts that simplify to true are excluded
2011-06-20, by blanchet
slightly better setup for E
2011-06-20, by blanchet
respect "really_all" argument, which is used by "ATP_Export"
2011-06-20, by blanchet
slightly better setup for SPASS and Vampire as more results have come in
2011-06-20, by blanchet
optimized SPASS and Vampire time slices, like E before
2011-06-20, by blanchet
optimized E's time slicing, based on latest exhaustive Judgment Day results
2011-06-20, by blanchet
deal with ATP time slices in a more flexible/robust fashion
2011-06-20, by blanchet
literal unicode in README.html allows to copy/paste from Lobo output;
2011-06-20, by wenzelm
merged;
2011-06-19, by wenzelm
explain special control symbols;
2011-06-19, by wenzelm
accept control symbols;
2011-06-19, by wenzelm
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
2011-06-19, by blanchet
recognize one more E failure message
2011-06-19, by blanchet
tweaked TPTP formula kind for typing information used in the conjecture
2011-06-19, by blanchet
more forceful message
2011-06-19, by blanchet
treat quotes as non-controllable, to reduce surprise in incremental editing;
2011-06-19, by wenzelm
abbreviations for special control symbols;
2011-06-19, by wenzelm
completion for control symbols;
2011-06-19, by wenzelm
updated to jedit_build-20110619;
2011-06-19, by wenzelm
support for bold style within text buffer;
2011-06-19, by wenzelm
tuned;
2011-06-19, by wenzelm
discontinued special treatment of \<^loc> (which was original meant as workaround for "local" syntax);
2011-06-19, by wenzelm
added glyphs 21e0..21e4, 21e6..21e9, 2759 from DejaVuSansMono;
2011-06-19, by wenzelm
names for control symbols without "^", which is relevant for completion;
2011-06-19, by wenzelm
some unicode chars for special control symbols;
2011-06-19, by wenzelm
tuned;
2011-06-19, by wenzelm
tuned markup;
2011-06-18, by wenzelm
avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
2011-06-18, by wenzelm
proper gfx.setColor;
2011-06-18, by wenzelm
proper x1;
2011-06-18, by wenzelm
convenience functions;
2011-06-18, by wenzelm
more robust caret painting wrt. surrogate characters;
2011-06-18, by wenzelm
do not control malformed symbols;
2011-06-18, by wenzelm
Buffer.editSyntaxStyle: mask extended syntax styles;
2011-06-18, by wenzelm
hardwired abbreviations for standard control symbols;
2011-06-18, by wenzelm
updated to jedit_build-20110618, which is required for sub/superscript rendering;
2011-06-18, by wenzelm
basic support for extended syntax styles: sub/superscript;
2011-06-18, by wenzelm
tuned -- Map.empty serves as partial function;
2011-06-18, by wenzelm
proper place for config files (cf. 55866987a7d9);
2011-06-18, by wenzelm
tuned signature;
2011-06-18, by wenzelm
merged
2011-06-18, by wenzelm
IMP compiler with int, added reverse soundness direction
2011-06-17, by kleing
proper place for config files;
2011-06-18, by wenzelm
tuned markup;
2011-06-18, by wenzelm
highlight via foreground painter, using alpha channel;
2011-06-18, by wenzelm
tuned signature;
2011-06-18, by wenzelm
tuned text;
2011-06-18, by wenzelm
inner literal/delimiter corresponds to outer keyword/operator;
2011-06-18, by wenzelm
tuned markup;
2011-06-18, by wenzelm
more uniform treatment of "keyword" vs. "operator";
2011-06-18, by wenzelm
simplified Line_Context (again);
2011-06-18, by wenzelm
more robust treatment of partial range restriction;
2011-06-18, by wenzelm
select_markup: no filtering here -- results may be distorted anyway;
2011-06-18, by wenzelm
more explicit treatment of ranges after revert/convert, which may well distort the overall start/end positions;
2011-06-17, by wenzelm
more explicit error message;
2011-06-17, by wenzelm
merged
2011-06-17, by wenzelm
gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"
2011-06-16, by blanchet
added missing case in pattern matching -- solves Waldmeister "Match" exceptions that have been plaguing some users
2011-06-16, by blanchet
fixed soundness bug related to extensionality
2011-06-16, by blanchet
unconditional recovery from bad context (e.g. Quoted with malformed quoted_body);
2011-06-17, by wenzelm
flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
2011-06-17, by wenzelm
recovered markup for non-alphabetic keywords;
2011-06-17, by wenzelm
more precise imitation of original TextAreaPainter: no locking;
2011-06-16, by wenzelm
more precise imitatation of original TokenMarker: no locking, interned context etc.;
2011-06-16, by wenzelm
brute-force range restriction to avoid spurious crashes;
2011-06-16, by wenzelm
static token markup, based on outer syntax only;
2011-06-16, by wenzelm
explicit dependency on Pure.jar;
2011-06-16, by wenzelm
partial scans of nested comments;
2011-06-16, by wenzelm
some support for partial scans with explicit context;
2011-06-16, by wenzelm
tuned spelling
2011-06-16, by haftmann
updated generated file;
2011-06-15, by wenzelm
merged
2011-06-15, by wenzelm
spelling
2011-06-15, by haftmann
avoid compiler warning -- this is unchecked anyway;
2011-06-15, by wenzelm
tuned messages;
2011-06-15, by wenzelm
uniform use of Document_View.robust_body;
2011-06-15, by wenzelm
merged
2011-06-15, by wenzelm
merge
2011-06-15, by blanchet
fixed soundness bug made more visible by previous change
2011-06-15, by blanchet
use more appropriate type systems for ATP exporter
2011-06-15, by blanchet
type arguments now (unlike back when fa2cf11d6351 was done) normally carry enough information to reconstruct the type of an applied constant, so no need to constraint the argument types in those cases
2011-06-15, by blanchet
more robust painter_body wrt. EBP races and spurious exceptions (which causes jEdit to remove the extension);
2011-06-15, by wenzelm
more robust init;
2011-06-15, by wenzelm
recovered orig_text_painter from f4141da52e92;
2011-06-15, by wenzelm
tuned;
2011-06-15, by wenzelm
more elaborate syntax styles;
2011-06-15, by wenzelm
more precise caret painting, working around existing painter (which is reinstalled by jEdit occasionally);
2011-06-15, by wenzelm
paint caret according to precise font metrics;
2011-06-15, by wenzelm
include scala mode;
2011-06-14, by wenzelm
builtin sub/superscript styles for jedit-4.3.2;
2011-06-14, by wenzelm
merged
2011-06-14, by wenzelm
tuned colors;
2011-06-14, by wenzelm
recovered tooltip Entity content (odd effect of layer change!? cf. 806878ae2219);
2011-06-14, by wenzelm
more foreground markup, using actual CSS color names;
2011-06-14, by wenzelm
slightly more general treatment of mutually recursive datatypes;
2011-06-14, by boehmes
more explicit check of dependencies;
2011-06-14, by wenzelm
tuned;
2011-06-14, by wenzelm
misc tuning and simplification;
2011-06-14, by wenzelm
separate module for text area painting;
2011-06-14, by wenzelm
improved mutabelle script to use nat for quickcheck_narrowing
2011-06-14, by bulwahn
quickcheck_narrowing returns some timing information
2011-06-14, by bulwahn
removed comment and declaration after issue has been resolved (cf. e83695ea0e0a)
2011-06-14, by bulwahn
more accurate CSS colors;
2011-06-13, by wenzelm
some direct text foreground painting, instead of token marking;
2011-06-13, by wenzelm
imitate original Chunk.paintChunkList;
2011-06-13, by wenzelm
tuned;
2011-06-13, by wenzelm
always use our text painter;
2011-06-13, by wenzelm
use orig_text_painter for extras outside main text (also required to update internal line infos);
2011-06-13, by wenzelm
more precise imitation of original TextAreaPainter$PaintText;
2011-06-12, by wenzelm
tuned;
2011-06-12, by wenzelm
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
2011-06-12, by wenzelm
check source dependencies only if jedit_build component is available;
2011-06-12, by wenzelm
cover method "deepen" concisely;
2011-06-11, by wenzelm
moved/updated single-step tactics;
2011-06-11, by wenzelm
tuned sections;
2011-06-11, by wenzelm
reverted 5fcd0ca1f582 -- isatest provides its own libgmp3 via LD_LIBRARY_PATH, which are also required for swipl;
2011-06-11, by wenzelm
tuned comment
2011-06-11, by haftmann
name tuning
2011-06-10, by blanchet
revived the lightweight "poly_tags_{query,bang}" type encodings by fixing their soundness bug
2011-06-10, by blanchet
don't trim proofs in debug mode
2011-06-10, by blanchet
tuning
2011-06-10, by blanchet
isatest/makedist: build Isabelle/jEdit;
2011-06-10, by wenzelm
makedist -j: build Isabelle/jEdit via given jedit_build component;
2011-06-10, by wenzelm
adding another narrowing strategy for integers
2011-06-10, by bulwahn
merged
2011-06-10, by wenzelm
pass --trim option to "eproof" script to speed up proof reconstruction
2011-06-10, by blanchet
removed "atp" and "atps" aliases, which users should have forgotten by now if they ever used them
2011-06-10, by blanchet
fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day
2011-06-10, by blanchet
compute the set of base facts only once (instead of three times in parallel) -- this saves about .5 s of CPU time, albeit much less clock wall time
2011-06-10, by blanchet
use existing ghc on macbroy20;
2011-06-10, by wenzelm
local gensym based on Name.variant;
2011-06-10, by wenzelm
uniform use of flexflex_rule;
2011-06-10, by wenzelm
tuned name (cf. blast_stats);
2011-06-10, by wenzelm
more official options blast_trace, blast_stats;
2011-06-10, by wenzelm
merged
2011-06-09, by wenzelm
merged
2011-06-09, by bulwahn
resolving an issue with class instances that are pseudo functions in the OCaml code serializer
2011-06-09, by bulwahn
merged
2011-06-09, by hoelzl
fixed document generation for HOL
2011-06-09, by hoelzl
lemma: independence is equal to mutual information = 0
2011-06-09, by hoelzl
jensens inequality
2011-06-09, by hoelzl
lemmas about right derivative and limits
2011-06-09, by hoelzl
lemma about differences of convex functions
2011-06-09, by hoelzl
lemmas relating ln x and x - 1
2011-06-09, by hoelzl
use divide instead of inverse for the derivative of ln
2011-05-31, by hoelzl
adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
2011-06-09, by bulwahn
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-06-09, by wenzelm
document depth arguments of method "auto";
2011-06-09, by wenzelm
clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
2011-06-09, by wenzelm
clarified special incr_type_indexes;
2011-06-09, by wenzelm
tuned signature: Name.invent and Name.invent_names;
2011-06-09, by wenzelm
modernized structure ProofContext;
2011-06-08, by wenzelm
even more robust \isaspacing;
2011-06-09, by wenzelm
simplified Name.variant -- discontinued builtin fold_map;
2011-06-09, by wenzelm
some attempts at robust \isaspacing so that \isa{...} can be used in section headings etc. (need to avoid `\? for some reason);
2011-06-09, by wenzelm
discontinued Name.variant to emphasize that this is old-style / indirect;
2011-06-09, by wenzelm
prefer new-style Name.invents;
2011-06-09, by wenzelm
more tight name invention -- avoiding old functions;
2011-06-09, by wenzelm
\frenchspacing for formal isabelle style avoids extra space in situations like ``@{text "?"}'' followed by plain text;
2011-06-09, by wenzelm
tuned;
2011-06-09, by wenzelm
NEWS
2011-06-09, by bulwahn
correcting import theory of examples
2011-06-09, by bulwahn
fixing code generation test
2011-06-09, by bulwahn
removing char setup
2011-06-09, by bulwahn
removing unneccessary manual instantiations and dead definitions; hiding more constants and facts
2011-06-09, by bulwahn
adding a nicer error message for quickcheck_narrowing; hiding fact empty_def
2011-06-09, by bulwahn
adding narrowing engine for existentials
2011-06-09, by bulwahn
adapting Quickcheck_Narrowing: adding setup for characters; correcting import statement
2011-06-09, by bulwahn
adding theory Quickcheck_Narrowing to HOL-Main image
2011-06-09, by bulwahn
adapting IsaMakefile
2011-06-09, by bulwahn
moving Quickcheck_Narrowing from Library to base directory
2011-06-09, by bulwahn
compilation of Haskell in its own target for Quickcheck; passing options by arguments in Narrowing_Generators
2011-06-09, by bulwahn
local simp rule in List_Cset
2011-06-09, by bulwahn
tuning
2011-06-09, by blanchet
compile
2011-06-09, by blanchet
cleaner fact freshening, which also works in corner cases, e.g. if two backquoted facts have the same name (but have different variable indices)
2011-06-09, by blanchet
added a really fully typed translation as a fallback for Metis, in rare cases where Metis correctly proves a theorem but has type-unsound steps in it (which is likelier to happen with some of the lighter translations)
2011-06-09, by blanchet
improve sort inference in Metis proofs -- in some rare cases Metis steals Isabelle's variable names and the sorts must then be inferred as well
2011-06-09, by blanchet
removed needless function that duplicated standard functionality, with a little unnecessary twist
2011-06-09, by blanchet
removed more dead code
2011-06-09, by blanchet
be a bit more liberal with respect to the universal sort -- it sometimes help
2011-06-09, by blanchet
renamed "untyped_aconv" to distinguish it clearly from the standard "aconv_untyped"
2011-06-09, by blanchet
merged
2011-06-08, by wenzelm
avoid duplicate facts, which confuse the minimizer output
2011-06-08, by blanchet
pass Metis facts and negated conjecture as facts, with (almost) correctly set localities, so that the correct encoding is used for nonmonotonic occurrences of infinite types
2011-06-08, by blanchet
restore comment about subtle issue
2011-06-08, by blanchet
made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
2011-06-08, by blanchet
don't launch the automatic minimizer for zero facts
2011-06-08, by blanchet
don't generate unsound proof error for missing proofs
2011-06-08, by blanchet
renamed option to avoid talking about seconds, since this is now the default Isabelle unit
2011-06-08, by blanchet
fixed format selection logic for Waldmeister
2011-06-08, by blanchet
better default type system for Waldmeister, with fewer predicates (for types or type classes)
2011-06-08, by blanchet
simplified directory structure;
2011-06-08, by wenzelm
simplified directory structure;
2011-06-08, by wenzelm
further jedit build option;
2011-06-08, by wenzelm
build jedit as part of regular startup script (in that case depending on jedit_build component);
2011-06-08, by wenzelm
updated headers;
2011-06-08, by wenzelm
moved sources -- eliminated Netbeans artifact of jedit package directory;
2011-06-08, by wenzelm
removed obsolete Netbeans project setup;
2011-06-08, by wenzelm
support fresh build of jars;
2011-06-08, by wenzelm
more jvmpath wrapping for Cygwin;
2011-06-08, by wenzelm
more robust exception pattern General.Subscript;
2011-06-08, by wenzelm
pervasive Output operations;
2011-06-08, by wenzelm
modernized Proof_Context;
2011-06-08, by wenzelm
standardized header;
2011-06-08, by wenzelm
merged
2011-06-08, by boehmes
updated SMT certificates
2011-06-08, by boehmes
only collect substituions neither seen before nor derived in the same refinement step
2011-06-08, by boehmes
updated imports (cf. 93b1183e43e5);
2011-06-08, by wenzelm
merged
2011-06-08, by wenzelm
new Metis version
2011-06-08, by blanchet
removed yet another hack in "make_metis" script -- respect opacity of "Metis_Name.name"
2011-06-08, by blanchet
exploit new semantics of "max_new_instances"
2011-06-08, by blanchet
minor optimization
2011-06-08, by blanchet
don't needlessly extensionalize
2011-06-08, by blanchet
don't needlessly presimplify -- makes ATP problem preparation much faster
2011-06-08, by blanchet
tuned
2011-06-08, by blanchet
removed experimental code submitted by mistake
2011-06-08, by blanchet
make sure that the message tail (timing + TPTP important message) is preserved upon automatic minimization
2011-06-08, by blanchet
removed removed option from documentation
2011-06-08, by blanchet
killed "explicit_apply" option in Sledgehammer -- the "smart" default is about as lightweight as "false" and just as complete as "true"
2011-06-08, by blanchet
slightly faster/cleaner accumulation of polymorphic consts
2011-06-08, by blanchet
eliminated unnecessary tail-recursion and funny use of records as 'named arguments' for functions
2011-06-08, by krauss
more conventional variable naming
2011-06-08, by krauss
dropped outdated/speculative historical comments;
2011-06-08, by krauss
less redundant tags
2011-06-08, by krauss
removed generation of instantiated pattern set, which is never actually used
2011-06-08, by krauss
more precise type for obscure "prfx" field
2011-06-08, by krauss
clarified (and slightly modified) the semantics of max_new_instances
2011-06-07, by boehmes
use null_heap instead of %_. 0 to avoid printing problems
2011-06-07, by kleing
prioritize more relevant facts for monomorphization
2011-06-07, by blanchet
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs
2011-06-07, by blanchet
workaround current "max_new_instances" semantics
2011-06-07, by blanchet
fixed missing proof handling
2011-06-07, by blanchet
optimized the relevance filter a little bit
2011-06-07, by blanchet
printing environment in mutabelle's log
2011-06-07, by bulwahn
merged
2011-06-07, by bulwahn
merged; manually merged IsaMakefile
2011-06-07, by bulwahn
splitting Cset into Cset and List_Cset
2011-06-07, by bulwahn
adding finitize_functions and processing of equivalences in existential compilation in quickcheck_narrowing
2011-06-07, by bulwahn
adding examples with existentials
2011-06-07, by bulwahn
renaming the formalisation of the birthday problem to a proper English name
2011-06-07, by bulwahn
adding compilation that allows existentials in Quickcheck_Narrowing
2011-06-07, by bulwahn
move away from old SMT monomorphizer
2011-06-07, by blanchet
tuning
2011-06-07, by blanchet
merged
2011-06-07, by blanchet
use the proper prover name, e.g. metis_full_types, not metis (full_types), for minimizing
2011-06-07, by blanchet
removed "verbose" option -- there won't be any verbosity in there, according to Sascha (yeah)
2011-06-07, by blanchet
nicely thread monomorphism verbosity in Metis and Sledgehammer
2011-06-07, by blanchet
clarified meaning of monomorphization configuration option by renaming it
2011-06-07, by boehmes
documentation tweaks
2011-06-07, by blanchet
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
2011-06-07, by blanchet
fixed typo in legacy feature message
2011-06-07, by blanchet
use new monomorphization code
2011-06-07, by blanchet
added (currently unused) verbose configuration option
2011-06-07, by blanchet
renamed ML function
2011-06-07, by blanchet
renamed example theory to "ATP_Export", for consistency with its underlying "ATP_" modules
2011-06-07, by blanchet
pass props not thms to ATP translator
2011-06-07, by blanchet
slighly more reasonable Vampire slices (until new monomorphizer is used)
2011-06-06, by blanchet
removed confusing slicing logic
2011-06-06, by blanchet
suggest first reconstructor that timed out, not last (i.e. metis not metisFT in most cases)
2011-06-06, by blanchet
effectively reenable slices for SPASS and Vampire -- they were disabled by mistake
2011-06-06, by blanchet
minor: curly brackets, not square brackets
2011-06-06, by blanchet
document metis better in Sledgehammer docs
2011-06-06, by blanchet
updated Sledgehammer message
2011-06-06, by blanchet