| 2010-08-01 |
blanchet |
fix minor bug in sym breaking
|
changeset |
files
|
| 2010-08-06 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| 2010-08-05 |
wenzelm |
Document_Model: include token marker here;
|
changeset |
files
|
| 2010-08-05 |
wenzelm |
tuned;
|
changeset |
files
|
| 2010-08-05 |
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
|
| 2010-08-05 |
wenzelm |
editor mode;
|
changeset |
files
|
| 2010-08-05 |
wenzelm |
Text_Edit.convert/revert;
|
changeset |
files
|
| 2010-08-05 |
wenzelm |
renamed to_current to convert, and from_current to revert;
|
changeset |
files
|
| 2010-08-05 |
wenzelm |
Change.Snapshot: include from_current/to_current here, with precomputed changes;
|
changeset |
files
|
| 2010-08-05 |
wenzelm |
explicit Change.Snapshot and Document.Node;
|
changeset |
files
|
| 2010-08-05 |
wenzelm |
simplified/refined document model: collection of named nodes, without proper dependencies yet;
|
changeset |
files
|
| 2010-08-05 |
wenzelm |
somewhat uniform Thy_Header.split_thy_path in ML and Scala;
|
changeset |
files
|
| 2010-08-04 |
wenzelm |
uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);
|
changeset |
files
|
| 2010-08-04 |
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
|
| 2010-08-04 |
wenzelm |
export use_thys_wrt;
|
changeset |
files
|
| 2010-08-04 |
wenzelm |
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
|
changeset |
files
|
| 2010-08-04 |
wenzelm |
updated to Netbeans 6.9;
|
changeset |
files
|
| 2010-08-04 |
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
|
| 2010-08-03 |
wenzelm |
more precise CRITICAL sections;
|
changeset |
files
|
| 2010-08-03 |
wenzelm |
removed unused Update_Time data (cf. ac94ff28e9e1);
|
changeset |
files
|
| 2010-08-03 |
wenzelm |
modernized specifications;
|
changeset |
files
|
| 2010-08-03 |
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
|
| 2010-08-03 |
wenzelm |
find_and_undo: no need to kill_thy again -- Thy_Info.toplevel_begin_theory does that initially (cf. 3ceccd415145);
|
changeset |
files
|
| 2010-08-03 |
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
|
| 2010-08-03 |
wenzelm |
tuned headers -- more precise load path;
|
changeset |
files
|
| 2010-08-03 |
wenzelm |
theory loading: only the master source file is looked-up in the implicit load path;
|
changeset |
files
|
| 2010-08-03 |
wenzelm |
load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;
|
changeset |
files
|
| 2010-08-03 |
wenzelm |
simplified/clarified Thy_Load path: search for master only, lookup other files relative to that;
|
changeset |
files
|
| 2010-08-03 |
bulwahn |
only test prolog code examples if environment variable is set
|
changeset |
files
|
| 2010-08-02 |
ballarin |
Revised proof of long division contributed by Jesus Aransay.
|
changeset |
files
|
| 2010-08-01 |
blanchet |
fix bug with Kodkodi < 1.2.14
|
changeset |
files
|
| 2010-08-01 |
blanchet |
merged
|
changeset |
files
|
| 2010-08-01 |
blanchet |
document new Nitpick options
|
changeset |
files
|
| 2010-08-01 |
blanchet |
tweak datatype sym break code
|
changeset |
files
|
| 2010-08-01 |
blanchet |
added manual symmetry breaking for datatypes
|
changeset |
files
|
| 2010-07-31 |
blanchet |
change the order of the SAT solvers, from fastest to slowest
|
changeset |
files
|
| 2010-07-31 |
blanchet |
started implementation of custom sym break
|
changeset |
files
|
| 2010-07-31 |
blanchet |
clarify Nitpick's output in case of a potential counterexample
|
changeset |
files
|
| 2010-07-30 |
blanchet |
added support for CryptoMiniSat
|
changeset |
files
|
| 2010-07-30 |
blanchet |
gracefully handle the case where no integers occur in the formula and the "max" option is used
|
changeset |
files
|
| 2010-08-01 |
bulwahn |
merged
|
changeset |
files
|
| 2010-08-01 |
bulwahn |
adding Code_Prolog theory to IsaMakefile and HOL-Library root file
|
changeset |
files
|
| 2010-08-01 |
bulwahn |
inductive_simps learns to have more tool compliance
|
changeset |
files
|
| 2010-08-01 |
bulwahn |
setting up Code_Prolog_Examples
|
changeset |
files
|
| 2010-08-01 |
bulwahn |
adding queens and symbolic derivation example for prolog code generation
|
changeset |
files
|
| 2010-08-01 |
bulwahn |
adding parsing of numbers; improving output of solution without free variables in prolog code generation
|
changeset |
files
|
| 2010-08-01 |
bulwahn |
adding preprocessing of introduction rules to replace the constant Predicate.eq in the prolog code generation
|
changeset |
files
|
| 2010-08-01 |
bulwahn |
adding basic arithmetic support for prolog code generation
|
changeset |
files
|
| 2010-08-01 |
bulwahn |
adding numbers as basic term in prolog code generation
|
changeset |
files
|
| 2010-07-31 |
ballarin |
More consistent naming of locale api functions.
|
changeset |
files
|
| 2010-07-31 |
ballarin |
Documentation of 'interpret' updated.
|
changeset |
files
|
| 2010-07-31 |
ballarin |
print_interps shows interpretations in proofs.
|
changeset |
files
|
| 2010-07-31 |
ballarin |
Interpretation in proofs supports mixins.
|
changeset |
files
|
| 2010-07-31 |
ballarin |
Make registrations generic data.
|
changeset |
files
|
| 2010-07-30 |
blanchet |
merged
|
changeset |
files
|
| 2010-07-29 |
blanchet |
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
|
changeset |
files
|
| 2010-07-29 |
blanchet |
fix Mirabelle timeout
|
changeset |
files
|
| 2010-07-29 |
blanchet |
make Mirabelle happy
|
changeset |
files
|
| 2010-07-29 |
blanchet |
fix bug in the newly introduced "bound concealing" code
|
changeset |
files
|
| 2010-07-29 |
blanchet |
handle division by zero gracefully (used to raise Unordered later on)
|
changeset |
files
|