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;