2010-08-03 blanchet 2010-08-03 speed up Nitpick examples a little bit
2010-08-03 blanchet 2010-08-03 minor changes
2010-08-03 blanchet 2010-08-03 updated example timings
2010-08-03 blanchet 2010-08-03 more helpful message
2010-08-03 blanchet 2010-08-03 also mention gfp
2010-08-03 blanchet 2010-08-03 bump up the max cardinalities, to use up more of the time given to us by the user
2010-08-03 blanchet 2010-08-03 make tracing monotonicity easier
2010-08-03 blanchet 2010-08-03 more documentation, based on email discussions with a user
2010-08-03 blanchet 2010-08-03 make example easier to parse
2010-08-03 blanchet 2010-08-03 clarify attribute documentation
2010-08-03 blanchet 2010-08-03 choose better example
2010-08-03 blanchet 2010-08-03 fix newly introduced bug w.r.t. conditional equations
2010-08-03 blanchet 2010-08-03 document something I explained in an email to a poweruser
2010-08-03 blanchet 2010-08-03 make Nitpick more flexible when parsing (p)simp rules
2010-08-03 blanchet 2010-08-03 fix soundness bug w.r.t. "Suc" with "binary_ints"
2010-08-03 blanchet 2010-08-03 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
2010-08-03 blanchet 2010-08-03 optimize local "def"s by treating them as definitions
2010-08-02 blanchet 2010-08-02 careful about which linear inductive predicates should be starred
2010-08-02 blanchet 2010-08-02 help Nitpick
2010-08-02 blanchet 2010-08-02 fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
2010-08-02 blanchet 2010-08-02 prevent generation of needless specialized constants etc.
2010-08-02 blanchet 2010-08-02 optimize generated Kodkod formula
2010-08-02 blanchet 2010-08-02 prefer implication to equality, to be more SAT solver friendly
2010-08-02 blanchet 2010-08-02 minor symmetry breaking for codatatypes like llist
2010-08-02 blanchet 2010-08-02 fix bug with mutually recursive and nested codatatypes
2010-08-01 blanchet 2010-08-01 fix minor bug in sym breaking
2010-08-06 wenzelm 2010-08-06 modernized specifications; tuned headers;
2010-08-05 wenzelm 2010-08-05 Document_Model: include token marker here;
2010-08-05 wenzelm 2010-08-05 tuned;
2010-08-05 wenzelm 2010-08-05 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 wenzelm 2010-08-05 editor mode;
2010-08-05 wenzelm 2010-08-05 Text_Edit.convert/revert;
2010-08-05 wenzelm 2010-08-05 renamed to_current to convert, and from_current to revert;
2010-08-05 wenzelm 2010-08-05 Change.Snapshot: include from_current/to_current here, with precomputed changes;
2010-08-05 wenzelm 2010-08-05 explicit Change.Snapshot and Document.Node; misc tuning and clarification; Document_View: explicitly highlight outdated command status;
2010-08-05 wenzelm 2010-08-05 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;
2010-08-05 wenzelm 2010-08-05 somewhat uniform Thy_Header.split_thy_path in ML and Scala;
2010-08-04 wenzelm 2010-08-04 uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);
2010-08-04 wenzelm 2010-08-04 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 wenzelm 2010-08-04 export use_thys_wrt;
2010-08-04 wenzelm 2010-08-04 more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
2010-08-04 wenzelm 2010-08-04 updated to Netbeans 6.9;
2010-08-04 wenzelm 2010-08-04 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-03 wenzelm 2010-08-03 more precise CRITICAL sections; tuned;
2010-08-03 wenzelm 2010-08-03 removed unused Update_Time data (cf. ac94ff28e9e1);
2010-08-03 wenzelm 2010-08-03 modernized specifications; tuned headers;
2010-08-03 wenzelm 2010-08-03 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 wenzelm 2010-08-03 find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
2010-08-03 wenzelm 2010-08-03 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 wenzelm 2010-08-03 tuned headers -- more precise load path;
2010-08-03 wenzelm 2010-08-03 theory loading: only the master source file is looked-up in the implicit load path;
2010-08-03 wenzelm 2010-08-03 load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;
2010-08-03 wenzelm 2010-08-03 simplified/clarified Thy_Load path: search for master only, lookup other files relative to that; tuned;
2010-08-03 bulwahn 2010-08-03 only test prolog code examples if environment variable is set
2010-08-02 ballarin 2010-08-02 Revised proof of long division contributed by Jesus Aransay.
2010-08-01 blanchet 2010-08-01 fix bug with Kodkodi < 1.2.14
2010-08-01 blanchet 2010-08-01 merged
2010-08-01 blanchet 2010-08-01 document new Nitpick options
2010-08-01 blanchet 2010-08-01 tweak datatype sym break code
2010-08-01 blanchet 2010-08-01 added manual symmetry breaking for datatypes