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

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
move function to library
2013-05-07, by blanchet
tuning
2013-05-07, by blanchet
more
2013-05-07, by blanchet
tuning
2013-05-07, by blanchet
code tuning
2013-05-07, by blanchet
merge
2013-05-07, by blanchet
refactoring
2013-05-07, by blanchet
export one more function + tuning
2013-05-07, by blanchet
do not unfold the definition of the relator as it is not defined in terms of srel anymore
2013-05-07, by traytel
tuned
2013-05-07, by traytel
got rid of the set based relator---use (binary) predicate based relator instead
2013-05-07, by traytel
tuned names + extended ML signature
2013-05-07, by blanchet
merged
2013-05-07, by nipkow
tuned name: filter -> constrain (longer but more intuitive)
2013-05-07, by nipkow
tuning
2013-05-07, by blanchet
imported patch refactor_coiter_constr
2013-05-07, by blanchet
tuned
2013-05-07, by nipkow
started factoring out coiter construction
2013-05-06, by blanchet
rationalize ML signature
2013-05-06, by blanchet
factor out construction of iterator
2013-05-06, by blanchet
tuning
2013-05-06, by blanchet
improved defns and proofs
2013-05-06, by nipkow
undo 46d911ab9170 since it causes problems
2013-05-06, by smolkas
allow '-'s in tptp ids to avoid problems with remote_vampire
2013-05-06, by smolkas
added preplay tracing
2013-05-06, by smolkas
handle dummy atp terms
2013-05-06, by smolkas
avoid dummy annotations; terminate preplay/compression if metis fails; fixed bug
2013-05-06, by smolkas
added informative error messages
2013-05-06, by smolkas

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

isabelle