more docs

prevent the expansion of too large definitions -- use equations for these instead

make nitpick accept "==" for "nitpick_(p)simp"s

fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization

deal correctly with Pure.conjunction in mono check

rename internal functions

remove buggy and needless condition

renamed internal function

Cycle breaking in the bounds takes care of singly recursive datatypes, so we don't need to do it again; the effect of removing the constraint varies on problem to problem, but it tends to be overwhelmingly negative in conjuction with the new datatype sym breaking stuff at high cardinalities

avoid "<=>" in sym break constraint generation (since these are SAT-unfreundlich) + fix "epsilon2" to "epsilon1" (subtle bug)

improve datatype symmetry breaking; all based on "datatype bin_list = BNil | B0Cons bin_list | B1Cons bin_list" example

merged

make SML/NJ happy

get rid of all "optimizations" regarding "unit" and other cardinality-1 types

tuning

better "Pretty" handling

change formula for enumerating scopes

example tweaking -- also prevents Nitpick_Tests from using more than 1 thread

speed up Nitpick examples a little bit

minor changes

updated example timings

more helpful message

also mention gfp

bump up the max cardinalities, to use up more of the time given to us by the user

make tracing monotonicity easier

more documentation, based on email discussions with a user

make example easier to parse

clarify attribute documentation

choose better example

fix newly introduced bug w.r.t. conditional equations

document something I explained in an email to a poweruser

make Nitpick more flexible when parsing (p)simp rules

fix soundness bug w.r.t. "Suc" with "binary_ints"

handle free variables even more gracefully; 1. show those that only occur in assumptions as part of the constants; 2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld

optimize local "def"s by treating them as definitions

careful about which linear inductive predicates should be starred

help Nitpick

fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors

prevent generation of needless specialized constants etc.

optimize generated Kodkod formula

prefer implication to equality, to be more SAT solver friendly

minor symmetry breaking for codatatypes like llist

fix bug with mutually recursive and nested codatatypes

fix minor bug in sym breaking

modernized specifications; tuned headers;

Document_Model: include token marker here;

tuned;

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);

editor mode;

Text_Edit.convert/revert;

renamed to_current to convert, and from_current to revert;

Change.Snapshot: include from_current/to_current here, with precomputed changes;

explicit Change.Snapshot and Document.Node; misc tuning and clarification; Document_View: explicitly highlight outdated command status;

simplified/refined document model: collection of named nodes, without proper dependencies yet; moved basic type definitions for ids and edits from Isar_Document to Document; removed begin_document/end_document for now -- nodes emerge via edits; edits refer to named nodes explicitly;

somewhat uniform Thy_Header.split_thy_path in ML and Scala;

uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);

load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;

export use_thys_wrt;

more precise CRITICAL sections, using NAMED_CRITICAL uniformly;

updated to Netbeans 6.9;

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;

more precise CRITICAL sections; tuned;

removed unused Update_Time data (cf. ac94ff28e9e1);

modernized specifications; tuned headers;

eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;

find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);

renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);

tuned headers -- more precise load path;

theory loading: only the master source file is looked-up in the implicit load path;

load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;

simplified/clarified Thy_Load path: search for master only, lookup other files relative to that; tuned;

only test prolog code examples if environment variable is set

Revised proof of long division contributed by Jesus Aransay.

fix bug with Kodkodi < 1.2.14

merged

document new Nitpick options

tweak datatype sym break code

added manual symmetry breaking for datatypes

change the order of the SAT solvers, from fastest to slowest

started implementation of custom sym break

clarify Nitpick's output in case of a potential counterexample

added support for CryptoMiniSat

gracefully handle the case where no integers occur in the formula and the "max" option is used

merged

adding Code_Prolog theory to IsaMakefile and HOL-Library root file

inductive_simps learns to have more tool compliance

setting up Code_Prolog_Examples

adding queens and symbolic derivation example for prolog code generation

adding parsing of numbers; improving output of solution without free variables in prolog code generation

adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation

adding basic arithmetic support for prolog code generation

adding numbers as basic term in prolog code generation

More consistent naming of locale api functions.

Documentation of 'interpret' updated.

print_interps shows interpretations in proofs.

Interpretation in proofs supports mixins.

Make registrations generic data.

merged

don't choke on synonyms when parsing SPASS's Flotter output + renamings; the output format isn't documented so it was hard to guess that a single clause could be associated with several names...

fix Mirabelle timeout

make Mirabelle happy

fix bug in the newly introduced "bound concealing" code

handle division by zero gracefully (used to raise Unordered later on)

use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures; this replaces the previous, somewhat messy solution of adding "extra" clauses

fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)

handle schematic vars the same way in Sledgehammer as in Metis, to avoid unreplayable proofs

revert exception throwing in FOL_SOLVE, since they're not caught anyway

avoid "ATP Error: Error: blah" style messages

avoid "_def_raw" theorems

better error and minimizer output

deal with chained facts more gracefully

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"