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