isabelle: Graph

handle inductive predicates correctly after change in "def" semantics
2010-08-05, by blanchet
don't specialize built-ins or constructors
2010-08-05, by blanchet
more docs
2010-08-05, by blanchet
prevent the expansion of too large definitions -- use equations for these instead
2010-08-05, by blanchet
make nitpick accept "==" for "nitpick_(p)simp"s
2010-08-05, by blanchet
fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
2010-08-05, by blanchet
deal correctly with Pure.conjunction in mono check
2010-08-05, by blanchet
rename internal functions
2010-08-05, by blanchet
remove buggy and needless condition
2010-08-05, by blanchet
renamed internal function
2010-08-05, by blanchet
Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again;
2010-08-04, by blanchet
avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)
2010-08-04, by blanchet
improve datatype symmetry breaking;
2010-08-04, by blanchet
merged
2010-08-04, by blanchet
make SML/NJ happy
2010-08-04, by blanchet
get rid of all "optimizations" regarding "unit" and other cardinality-1 types
2010-08-04, by blanchet
tuning
2010-08-03, by blanchet
better "Pretty" handling
2010-08-03, by blanchet
change formula for enumerating scopes
2010-08-03, by blanchet
example tweaking -- also prevents Nitpick_Tests from using more than 1 thread
2010-08-03, by blanchet
speed up Nitpick examples a little bit
2010-08-03, by blanchet
minor changes
2010-08-03, by blanchet
updated example timings
2010-08-03, by blanchet
more helpful message
2010-08-03, by blanchet
also mention gfp
2010-08-03, by blanchet
bump up the max cardinalities, to use up more of the time given to us by the user
2010-08-03, by blanchet
make tracing monotonicity easier
2010-08-03, by blanchet
more documentation, based on email discussions with a user
2010-08-03, by blanchet
make example easier to parse
2010-08-03, by blanchet
clarify attribute documentation
2010-08-03, by blanchet
choose better example
2010-08-03, by blanchet
fix newly introduced bug w.r.t. conditional equations
2010-08-03, by blanchet
document something I explained in an email to a poweruser
2010-08-03, by blanchet
make Nitpick more flexible when parsing (p)simp rules
2010-08-03, by blanchet
fix soundness bug w.r.t. "Suc" with "binary_ints"
2010-08-03, by blanchet
handle free variables even more gracefully;
2010-08-03, by blanchet
optimize local "def"s by treating them as definitions
2010-08-03, by blanchet
careful about which linear inductive predicates should be starred
2010-08-02, by blanchet
help Nitpick
2010-08-02, by blanchet
fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
2010-08-02, by blanchet
prevent generation of needless specialized constants etc.
2010-08-02, by blanchet
optimize generated Kodkod formula
2010-08-02, by blanchet
prefer implication to equality, to be more SAT solver friendly
2010-08-02, by blanchet
minor symmetry breaking for codatatypes like llist
2010-08-02, by blanchet
fix bug with mutually recursive and nested codatatypes
2010-08-02, by blanchet
fix minor bug in sym breaking
2010-08-01, by blanchet
modernized specifications;
2010-08-06, by wenzelm
Document_Model: include token marker here;
2010-08-05, by wenzelm
tuned;
2010-08-05, by wenzelm
misc tuning -- produce reverse_edits at most once (note that foldRight produces a reversed list internally, while recursion is infisible due to small stack vs. large stack frames on JVM);
2010-08-05, by wenzelm
editor mode;
2010-08-05, by wenzelm
Text_Edit.convert/revert;
2010-08-05, by wenzelm
renamed to_current to convert, and from_current to revert;
2010-08-05, by wenzelm
Change.Snapshot: include from_current/to_current here, with precomputed changes;
2010-08-05, by wenzelm
explicit Change.Snapshot and Document.Node;
2010-08-05, by wenzelm
simplified/refined document model: collection of named nodes, without proper dependencies yet;
2010-08-05, by wenzelm
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
2010-08-05, by wenzelm
uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);
2010-08-04, by wenzelm
load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;
2010-08-04, by wenzelm
export use_thys_wrt;
2010-08-04, by wenzelm
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
2010-08-04, by wenzelm
updated to Netbeans 6.9;
2010-08-04, by wenzelm
schedule_futures: discontinued special treatment of non-parallel proofs, which might have affected memory usage at some point, but does not seem to make a difference with as little as 2GB RAM;
2010-08-04, by wenzelm
more precise CRITICAL sections;
2010-08-03, by wenzelm
removed unused Update_Time data (cf. ac94ff28e9e1);
2010-08-03, by wenzelm
modernized specifications;
2010-08-03, by wenzelm
eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;
2010-08-03, by wenzelm
find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
2010-08-03, by wenzelm
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
2010-08-03, by wenzelm
tuned headers -- more precise load path;
2010-08-03, by wenzelm
theory loading: only the master source file is looked-up in the implicit load path;
2010-08-03, by wenzelm
load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;
2010-08-03, by wenzelm
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
2010-08-03, by wenzelm
only test prolog code examples if environment variable is set
2010-08-03, by bulwahn
Revised proof of long division contributed by Jesus Aransay.
2010-08-02, by ballarin
fix bug with Kodkodi < 1.2.14
2010-08-01, by blanchet
merged
2010-08-01, by blanchet
document new Nitpick options
2010-08-01, by blanchet
tweak datatype sym break code
2010-08-01, by blanchet
added manual symmetry breaking for datatypes
2010-08-01, by blanchet
change the order of the SAT solvers, from fastest to slowest
2010-07-31, by blanchet
started implementation of custom sym break
2010-07-31, by blanchet
clarify Nitpick's output in case of a potential counterexample
2010-07-31, by blanchet
added support for CryptoMiniSat
2010-07-31, by blanchet
gracefully handle the case where no integers occur in the formula and the "max" option is used
2010-07-30, by blanchet
merged
2010-08-01, by bulwahn
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
2010-08-01, by bulwahn
inductive_simps learns to have more tool compliance
2010-08-01, by bulwahn
setting up Code_Prolog_Examples
2010-08-01, by bulwahn
adding queens and symbolic derivation example for prolog code generation
2010-08-01, by bulwahn
adding parsing of numbers; improving output of solution without free variables in prolog code generation
2010-08-01, by bulwahn
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
2010-08-01, by bulwahn
adding basic arithmetic support for prolog code generation
2010-08-01, by bulwahn
adding numbers as basic term in prolog code generation
2010-08-01, by bulwahn
More consistent naming of locale api functions.
2010-07-31, by ballarin
Documentation of 'interpret' updated.
2010-07-31, by ballarin
print_interps shows interpretations in proofs.
2010-07-31, by ballarin
Interpretation in proofs supports mixins.
2010-07-31, by ballarin
Make registrations generic data.
2010-07-31, by ballarin
merged
2010-07-30, by blanchet
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
2010-07-30, by blanchet
fix Mirabelle timeout
2010-07-29, by blanchet
make Mirabelle happy
2010-07-29, by blanchet
fix bug in the newly introduced "bound concealing" code
2010-07-29, by blanchet
handle division by zero gracefully (used to raise Unordered later on)
2010-07-29, by blanchet
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
2010-07-29, by blanchet
fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
2010-07-29, by blanchet
handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs
2010-07-29, by blanchet
revert exception throwing in FOL_SOLVE, since they're not caught anyway
2010-07-29, by blanchet
avoid "ATP Error: Error: blah" style messages
2010-07-29, by blanchet
avoid "_def_raw" theorems
2010-07-29, by blanchet
better error and minimizer output
2010-07-29, by blanchet
deal with chained facts more gracefully
2010-07-29, by blanchet
speed up the minimizer by using the time taken for the first iteration as a timeout for the following iterations, and fix a subtle bug in "string_for_failure"
2010-07-29, by blanchet
work around atomization failures
2010-07-29, by blanchet
fiddle with the fudge factors, to get similar results as before
2010-07-29, by blanchet
perform the presimplification done by Metis.make_nnf in Sledgehammer again, to deal with "If" and similar constructs
2010-07-29, by blanchet
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)
2010-07-29, by blanchet
generate correct names for "$true" and "$false";
2010-07-29, by blanchet
don't assume canonical rule format
2010-07-29, by blanchet