| 2013-05-13 |
wenzelm |
clarified message when subgoals have been stripped -- unconditional;
|
changeset |
files
|
| 2013-05-13 |
wenzelm |
retain goal display options when printing error messages, to avoid breakdown for huge goals;
|
changeset |
files
|
| 2013-05-13 |
kuncar |
typo
|
changeset |
files
|
| 2013-05-13 |
kuncar |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
changeset |
files
|
| 2013-05-13 |
kuncar |
try to detect assumptions of transfer rules that are in a shape of a transfer rule
|
changeset |
files
|
| 2013-05-13 |
kuncar |
publish a private function
|
changeset |
files
|
| 2013-05-13 |
nipkow |
tuned names
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
re-init ISABELLE_PROCESS_OPTIONS to allow nested ISABELLE_PROCESS invocations, e.g. HOL-Mutabelle-ex;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
prefer standard Isabelle/ML operations;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
some system options as context-sensitive config options;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
load options for regular isabelle-process, not just for Isar loop (relevant for numerous low-level tools) -- NB: Isabelle_Process manages options via protocol message;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
support for system options as context-sensitive config options;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
tuned signature;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
tuned comments;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
support for options as preferences;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
more operations in accordance to Scala version;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
more systematic access to options default;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
full default options for Isabelle_Process and Build;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
decentralized historic settings;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
removed obsolete test_markup;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
Proof General interaction always uses Isar loop;
|
changeset |
files
|
| 2013-05-12 |
wenzelm |
proper context;
|
changeset |
files
|
| 2013-05-11 |
wenzelm |
merged
|
changeset |
files
|
| 2013-05-11 |
wenzelm |
more direct PGIP/Emacs processing and output;
|
changeset |
files
|
| 2013-05-11 |
wenzelm |
more direct interpretation of "askprefs" and "setpref", which appear to be the only PGIP command used in PG 3.7.1.1, 4.1, 4.2;
|
changeset |
files
|
| 2013-05-11 |
wenzelm |
removed redundant modules;
|
changeset |
files
|
| 2013-05-11 |
wenzelm |
removed some obsolete PGIP/PGEclipse material;
|
changeset |
files
|
| 2013-05-11 |
wenzelm |
never open structure Unsynchronized (cf. "implementation" manual);
|
changeset |
files
|
| 2013-05-11 |
wenzelm |
prefer explicitly qualified exceptions, which is particular important for robust handlers;
|
changeset |
files
|
| 2013-05-11 |
wenzelm |
avoid PolyML.makestring, even in dead code;
|
changeset |
files
|
| 2013-05-11 |
blanchet |
fixed bug introduced when reintroducing set constructor, and visible when applying <= to 2- or more-ary relations, e.g. "(R::'a=>'a=>bool) <= R"
|
changeset |
files
|
| 2013-05-10 |
kuncar |
don't apply an unnecessary morphism
|
changeset |
files
|
| 2013-05-10 |
nipkow |
tuned
|
changeset |
files
|
| 2013-05-09 |
traytel |
relator coinduction for codatatypes
|
changeset |
files
|
| 2013-05-09 |
nipkow |
standard ivl notation [l,h]
|
changeset |
files
|
| 2013-05-09 |
nipkow |
merged
|
changeset |
files
|
| 2013-05-08 |
nipkow |
tuned
|
changeset |
files
|
| 2013-05-08 |
blanchet |
avoid polymorphic uncurried aliases with more arguments than there are arguments in the most general type of a HOL constant, to dodge issues at declaration time
|
changeset |
files
|
| 2013-05-08 |
blanchet |
proper unmangling -- the bug is visible when "uncurried_aliases" is enabled with Alt-Ergo or Poly. SPASS
|
changeset |
files
|
| 2013-05-08 |
blanchet |
use right default for "uncurried_aliases" with polymorphic SPASS
|
changeset |
files
|
| 2013-05-08 |
traytel |
relator induction for datatypes
|
changeset |
files
|
| 2013-05-08 |
traytel |
store proper theorems even for fixed points that have no passive live variables
|
changeset |
files
|
| 2013-05-08 |
traytel |
stronger monotonicity property for relators
|
changeset |
files
|
| 2013-05-08 |
traytel |
make tactic actually work for op = as relator
|
changeset |
files
|
| 2013-05-08 |
nipkow |
tuned
|
changeset |
files
|
| 2013-05-08 |
nipkow |
hide Fin on output
|
changeset |
files
|
| 2013-05-07 |
blanchet |
removed dead argument
|
changeset |
files
|
| 2013-05-07 |
blanchet |
more robust iterator construction (needed for mutualized FPs)
|
changeset |
files
|
| 2013-05-07 |
blanchet |
tuning
|
changeset |
files
|
| 2013-05-07 |
traytel |
removed dead internal constants/theorems
|
changeset |
files
|
| 2013-05-07 |
blanchet |
removed tracing
|
changeset |
files
|
| 2013-05-07 |
blanchet |
export one more function
|
changeset |
files
|
| 2013-05-07 |
blanchet |
added field to record
|
changeset |
files
|
| 2013-05-07 |
blanchet |
tuning
|
changeset |
files
|
| 2013-05-07 |
blanchet |
removed dead code
|
changeset |
files
|
| 2013-05-07 |
blanchet |
move function to library
|
changeset |
files
|
| 2013-05-07 |
blanchet |
tuning
|
changeset |
files
|
| 2013-05-07 |
blanchet |
more
|
changeset |
files
|
| 2013-05-07 |
blanchet |
tuning
|
changeset |
files
|