| Tue, 17 Nov 2009 23:47:57 +0100 |
blanchet |
bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits;
|
changeset |
files
|
| Tue, 17 Nov 2009 22:51:00 +0100 |
blanchet |
merged
|
changeset |
files
|
| Tue, 17 Nov 2009 22:20:51 +0100 |
blanchet |
comment out debugging code in Nitpick
|
changeset |
files
|
| Tue, 17 Nov 2009 19:47:27 +0100 |
blanchet |
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
|
changeset |
files
|
| Tue, 17 Nov 2009 19:12:10 +0100 |
blanchet |
made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions
|
changeset |
files
|
| Tue, 17 Nov 2009 19:08:02 +0100 |
blanchet |
removed "debug := true" that shouldn't have been submitted in the first place
|
changeset |
files
|
| Tue, 17 Nov 2009 18:52:30 +0100 |
hoelzl |
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
|
changeset |
files
|
| Tue, 17 Nov 2009 18:25:05 +0100 |
blanchet |
merged
|
changeset |
files
|
| Tue, 17 Nov 2009 18:24:43 +0100 |
blanchet |
run Nitpick examples if Kodkodi is available
|
changeset |
files
|
| Tue, 17 Nov 2009 15:55:30 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Tue, 17 Nov 2009 14:10:31 +0100 |
blanchet |
fixed "expect" of Nitpick examples to reflect latest changes in Nitpick
|
changeset |
files
|
| Tue, 17 Nov 2009 13:51:56 +0100 |
blanchet |
merged
|
changeset |
files
|
| Tue, 17 Nov 2009 13:51:16 +0100 |
blanchet |
use SAT solver that's available everywhere for this example
|
changeset |
files
|
| Tue, 17 Nov 2009 13:50:46 +0100 |
blanchet |
invoke Kodkodi from Nitpick using new $KODKOD/bin/kodkodi script;
|
changeset |
files
|
| Tue, 17 Nov 2009 10:58:37 +0100 |
blanchet |
merged
|
changeset |
files
|
| Mon, 16 Nov 2009 11:03:08 +0100 |
blanchet |
added constraint for Eq^- in Nitpick's implementation of the monotonicity calculus
|
changeset |
files
|
| Mon, 16 Nov 2009 10:24:28 +0100 |
blanchet |
change the order in which Nitpick tries SAT solvers;
|
changeset |
files
|
| Tue, 17 Nov 2009 11:10:22 +0000 |
webertj |
Fixed splitting of div and mod on integers (split theorem differed from implementation).
|
changeset |
files
|
| Tue, 17 Nov 2009 10:18:51 +0000 |
webertj |
merged
|
changeset |
files
|
| Tue, 17 Nov 2009 10:17:53 +0000 |
webertj |
Fixed splitting of div and mod on integers (split theorem differed from implementation).
|
changeset |
files
|
| Tue, 17 Nov 2009 15:53:35 +0100 |
wenzelm |
init_theory: Runtime.controlled_execution for proper exception trace etc.;
|
changeset |
files
|
| Tue, 17 Nov 2009 14:51:57 +0100 |
wenzelm |
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
|
changeset |
files
|
| Tue, 17 Nov 2009 14:51:32 +0100 |
wenzelm |
implicit name space grouping for theory/local_theory transactions;
|
changeset |
files
|
| Tue, 17 Nov 2009 14:50:55 +0100 |
wenzelm |
uniform new_group/reset_group;
|
changeset |
files
|