isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

dummy PGIP id, which appears to be sufficient for PG/Emacs;
2013-05-13, by wenzelm
limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);
2013-05-13, by wenzelm
merged
2013-05-13, by wenzelm
option "goals_limit", with more uniform description;
2013-05-13, by wenzelm
clarified message when subgoals have been stripped -- unconditional;
2013-05-13, by wenzelm
retain goal display options when printing error messages, to avoid breakdown for huge goals;
2013-05-13, by wenzelm
typo
2013-05-13, by kuncar
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
2013-05-13, by kuncar
try to detect assumptions of transfer rules that are in a shape of a transfer rule
2013-05-13, by kuncar
publish a private function
2013-05-13, by kuncar
tuned names
2013-05-13, by nipkow
re-init ISABELLE_PROCESS_OPTIONS to allow nested ISABELLE_PROCESS invocations, e.g. HOL-Mutabelle-ex;
2013-05-12, by wenzelm
more standard Isabelle/ML operations -- avoid inaccurate Bool.fromString;
2013-05-12, by wenzelm
prefer standard Isabelle/ML operations;
2013-05-12, by wenzelm
some system options as context-sensitive config options;
2013-05-12, by 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;
2013-05-12, by wenzelm
support for system options as context-sensitive config options;
2013-05-12, by wenzelm
tuned signature;
2013-05-12, by wenzelm
tuned comments;
2013-05-12, by wenzelm
support for options as preferences;
2013-05-12, by wenzelm
more operations in accordance to Scala version;
2013-05-12, by wenzelm
more systematic access to options default;
2013-05-12, by wenzelm
full default options for Isabelle_Process and Build;
2013-05-12, by wenzelm
decentralized historic settings;
2013-05-12, by wenzelm
removed obsolete test_markup;
2013-05-12, by wenzelm
Proof General interaction always uses Isar loop;
2013-05-12, by wenzelm
proper context;
2013-05-12, by wenzelm
merged
2013-05-11, by wenzelm
more direct PGIP/Emacs processing and output;
2013-05-11, by 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;
2013-05-11, by wenzelm
removed redundant modules;
2013-05-11, by wenzelm
removed some obsolete PGIP/PGEclipse material;
2013-05-11, by wenzelm
never open structure Unsynchronized (cf. "implementation" manual);
2013-05-11, by wenzelm
prefer explicitly qualified exceptions, which is particular important for robust handlers;
2013-05-11, by wenzelm
avoid PolyML.makestring, even in dead code;
2013-05-11, by wenzelm
fixed bug introduced when reintroducing set constructor, and visible when applying <= to 2- or more-ary relations, e.g. "(R::'a=>'a=>bool) <= R"
2013-05-11, by blanchet
don't apply an unnecessary morphism
2013-05-10, by kuncar
tuned
2013-05-10, by nipkow
relator coinduction for codatatypes
2013-05-09, by traytel
standard ivl notation [l,h]
2013-05-09, by nipkow
merged
2013-05-09, by nipkow
tuned
2013-05-08, by nipkow
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
2013-05-08, by blanchet
proper unmangling -- the bug is visible when "uncurried_aliases" is enabled with Alt-Ergo or Poly. SPASS
2013-05-08, by blanchet
use right default for "uncurried_aliases" with polymorphic SPASS
2013-05-08, by blanchet
relator induction for datatypes
2013-05-08, by traytel
store proper theorems even for fixed points that have no passive live variables
2013-05-08, by traytel
stronger monotonicity property for relators
2013-05-08, by traytel
make tactic actually work for op = as relator
2013-05-08, by traytel
tuned
2013-05-08, by nipkow
hide Fin on output
2013-05-08, by nipkow
removed dead argument
2013-05-07, by blanchet
more robust iterator construction (needed for mutualized FPs)
2013-05-07, by blanchet
tuning
2013-05-07, by blanchet
removed dead internal constants/theorems
2013-05-07, by traytel
removed tracing
2013-05-07, by blanchet
export one more function
2013-05-07, by blanchet
added field to record
2013-05-07, by blanchet
tuning
2013-05-07, by blanchet
removed dead code
2013-05-07, by blanchet

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip

isabelle