| Tue, 03 Aug 2010 12:16:32 +0200 |
blanchet |
fix soundness bug w.r.t. "Suc" with "binary_ints"
|
changeset |
files
|
| Tue, 03 Aug 2010 02:18:05 +0200 |
blanchet |
handle free variables even more gracefully;
|
changeset |
files
|
| Tue, 03 Aug 2010 01:16:08 +0200 |
blanchet |
optimize local "def"s by treating them as definitions
|
changeset |
files
|
| Mon, 02 Aug 2010 19:15:15 +0200 |
blanchet |
careful about which linear inductive predicates should be starred
|
changeset |
files
|
| Mon, 02 Aug 2010 18:52:51 +0200 |
blanchet |
help Nitpick
|
changeset |
files
|
| Mon, 02 Aug 2010 18:39:14 +0200 |
blanchet |
fix Skolemizer -- last week's optimizations resulted in UnequalLengths errors
|
changeset |
files
|
| Mon, 02 Aug 2010 16:29:36 +0200 |
blanchet |
prevent generation of needless specialized constants etc.
|
changeset |
files
|
| Mon, 02 Aug 2010 15:52:32 +0200 |
blanchet |
optimize generated Kodkod formula
|
changeset |
files
|
| Mon, 02 Aug 2010 14:27:20 +0200 |
blanchet |
prefer implication to equality, to be more SAT solver friendly
|
changeset |
files
|
| Mon, 02 Aug 2010 13:48:22 +0200 |
blanchet |
minor symmetry breaking for codatatypes like llist
|
changeset |
files
|
| Mon, 02 Aug 2010 12:36:50 +0200 |
blanchet |
fix bug with mutually recursive and nested codatatypes
|
changeset |
files
|
| Sun, 01 Aug 2010 23:15:26 +0200 |
blanchet |
fix minor bug in sym breaking
|
changeset |
files
|
| Fri, 06 Aug 2010 12:37:00 +0200 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Thu, 05 Aug 2010 23:43:43 +0200 |
wenzelm |
Document_Model: include token marker here;
|
changeset |
files
|
| Thu, 05 Aug 2010 22:01:25 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 05 Aug 2010 21:56:38 +0200 |
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);
|
changeset |
files
|
| Thu, 05 Aug 2010 21:40:20 +0200 |
wenzelm |
editor mode;
|
changeset |
files
|
| Thu, 05 Aug 2010 18:17:59 +0200 |
wenzelm |
Text_Edit.convert/revert;
|
changeset |
files
|
| Thu, 05 Aug 2010 18:13:12 +0200 |
wenzelm |
renamed to_current to convert, and from_current to revert;
|
changeset |
files
|
| Thu, 05 Aug 2010 18:00:37 +0200 |
wenzelm |
Change.Snapshot: include from_current/to_current here, with precomputed changes;
|
changeset |
files
|
| Thu, 05 Aug 2010 16:58:18 +0200 |
wenzelm |
explicit Change.Snapshot and Document.Node;
|
changeset |
files
|
| Thu, 05 Aug 2010 14:35:35 +0200 |
wenzelm |
simplified/refined document model: collection of named nodes, without proper dependencies yet;
|
changeset |
files
|
| Thu, 05 Aug 2010 13:41:00 +0200 |
wenzelm |
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
|
changeset |
files
|
| Wed, 04 Aug 2010 16:28:45 +0200 |
wenzelm |
uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);
|
changeset |
files
|
| Wed, 04 Aug 2010 16:11:51 +0200 |
wenzelm |
load_thy/after_load: explicit check of parent theories, which might have failed to join proofs -- avoid uninformative crash via Graph.UNDEF;
|
changeset |
files
|
| Wed, 04 Aug 2010 15:50:55 +0200 |
wenzelm |
export use_thys_wrt;
|
changeset |
files
|
| Wed, 04 Aug 2010 15:45:49 +0200 |
wenzelm |
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
|
changeset |
files
|
| Wed, 04 Aug 2010 15:14:48 +0200 |
wenzelm |
updated to Netbeans 6.9;
|
changeset |
files
|
| Wed, 04 Aug 2010 14:46:17 +0200 |
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;
|
changeset |
files
|
| Tue, 03 Aug 2010 22:28:43 +0200 |
wenzelm |
more precise CRITICAL sections;
|
changeset |
files
|
| Tue, 03 Aug 2010 21:34:38 +0200 |
wenzelm |
removed unused Update_Time data (cf. ac94ff28e9e1);
|
changeset |
files
|
| Tue, 03 Aug 2010 18:52:42 +0200 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| Tue, 03 Aug 2010 18:13:57 +0200 |
wenzelm |
eliminated Thy_Info.thy_ord, which is not really stable in interactive mode, since it depends on the somewhat accidental load order;
|
changeset |
files
|
| Tue, 03 Aug 2010 18:10:18 +0200 |
wenzelm |
find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
|
changeset |
files
|
| Tue, 03 Aug 2010 16:57:45 +0200 |
wenzelm |
renamed funny Library ROOT files back to default ROOT.ML -- ML files are no longer located via implicit load path (cf. 2b9bfa0b44f1);
|
changeset |
files
|
| Tue, 03 Aug 2010 16:48:36 +0200 |
wenzelm |
tuned headers -- more precise load path;
|
changeset |
files
|
| Tue, 03 Aug 2010 16:33:11 +0200 |
wenzelm |
theory loading: only the master source file is looked-up in the implicit load path;
|
changeset |
files
|
| Tue, 03 Aug 2010 16:21:33 +0200 |
wenzelm |
load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;
|
changeset |
files
|
| Tue, 03 Aug 2010 15:53:36 +0200 |
wenzelm |
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
|
changeset |
files
|
| Tue, 03 Aug 2010 08:23:08 +0200 |
bulwahn |
only test prolog code examples if environment variable is set
|
changeset |
files
|
| Mon, 02 Aug 2010 22:24:19 +0200 |
ballarin |
Revised proof of long division contributed by Jesus Aransay.
|
changeset |
files
|
| Sun, 01 Aug 2010 18:57:49 +0200 |
blanchet |
fix bug with Kodkodi < 1.2.14
|
changeset |
files
|
| Sun, 01 Aug 2010 17:43:51 +0200 |
blanchet |
merged
|
changeset |
files
|
| Sun, 01 Aug 2010 16:40:48 +0200 |
blanchet |
document new Nitpick options
|
changeset |
files
|
| Sun, 01 Aug 2010 16:35:25 +0200 |
blanchet |
tweak datatype sym break code
|
changeset |
files
|
| Sun, 01 Aug 2010 15:51:25 +0200 |
blanchet |
added manual symmetry breaking for datatypes
|
changeset |
files
|
| Sat, 31 Jul 2010 22:02:54 +0200 |
blanchet |
change the order of the SAT solvers, from fastest to slowest
|
changeset |
files
|
| Sat, 31 Jul 2010 16:39:32 +0200 |
blanchet |
started implementation of custom sym break
|
changeset |
files
|
| Sat, 31 Jul 2010 12:29:56 +0200 |
blanchet |
clarify Nitpick's output in case of a potential counterexample
|
changeset |
files
|
| Sat, 31 Jul 2010 01:23:51 +0200 |
blanchet |
added support for CryptoMiniSat
|
changeset |
files
|
| Fri, 30 Jul 2010 18:28:18 +0200 |
blanchet |
gracefully handle the case where no integers occur in the formula and the "max" option is used
|
changeset |
files
|
| Sun, 01 Aug 2010 10:26:55 +0200 |
bulwahn |
merged
|
changeset |
files
|
| Sun, 01 Aug 2010 10:15:44 +0200 |
bulwahn |
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
|
changeset |
files
|
| Sun, 01 Aug 2010 10:15:43 +0200 |
bulwahn |
inductive_simps learns to have more tool compliance
|
changeset |
files
|
| Sun, 01 Aug 2010 10:15:43 +0200 |
bulwahn |
setting up Code_Prolog_Examples
|
changeset |
files
|
| Sun, 01 Aug 2010 10:15:43 +0200 |
bulwahn |
adding queens and symbolic derivation example for prolog code generation
|
changeset |
files
|
| Sun, 01 Aug 2010 10:15:43 +0200 |
bulwahn |
adding parsing of numbers; improving output of solution without free variables in prolog code generation
|
changeset |
files
|
| Sun, 01 Aug 2010 10:15:43 +0200 |
bulwahn |
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
|
changeset |
files
|
| Sun, 01 Aug 2010 10:15:43 +0200 |
bulwahn |
adding basic arithmetic support for prolog code generation
|
changeset |
files
|
| Sun, 01 Aug 2010 10:15:43 +0200 |
bulwahn |
adding numbers as basic term in prolog code generation
|
changeset |
files
|