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

clarified preferences: "override" re-initialized on prover startup, and "default" sent to PG -- thus recover typical defaults like auto-quickcheck in PG 4.x;
2013-05-15, by wenzelm
simplified ProofGeneral.preference operation -- no need for CRITICAL section for atomic access (and sequential execution of PG/TTY loop);
2013-05-15, by wenzelm
back to hidden welcome -- revert change 9ebf2da69b29, which appears to disturb startup protocol of PG 4.1;
2013-05-15, by wenzelm
more standard Isabelle/ML structures for global preferences;
2013-05-15, by wenzelm
more basic print mode "ProofGeneral" (again);
2013-05-15, by wenzelm
uniform welcome -- actually visible on startup via Output.urgent_message;
2013-05-15, by wenzelm
more elementary ProofGeneral.thm_deps;
2013-05-15, by wenzelm
tuned;
2013-05-15, by wenzelm
moved files;
2013-05-15, by wenzelm
clarified default for Proofterm.proofs, according to etc/options and innermost setmp;
2013-05-15, by wenzelm
maintain ProofGeneral preferences within ProofGeneral module;
2013-05-15, by wenzelm
just one ProofGeneral module;
2013-05-15, by wenzelm
tuning
2013-05-15, by blanchet
more work on SPASS datatypes
2013-05-15, by blanchet
tuning
2013-05-15, by blanchet
no need to reinvent the wheel ("fold_map")
2013-05-15, by blanchet
more work on implementing datatype output for new SPASS
2013-05-15, by blanchet
tuned code
2013-05-15, by blanchet
compile
2013-05-15, by blanchet
renamed Sledgehammer functions with 'for' in their names to 'of'
2013-05-15, by blanchet
added datatype declaration syntax for next-gen SPASS
2013-05-15, by blanchet
abstract equalities only in a correspondence relation in a transfer domain rule
2013-05-15, by kuncar
superfluous transfer rule
2013-05-15, by kuncar
stronger reflexivity prover
2013-05-15, by kuncar
simplified modules and exceptions;
2013-05-14, by wenzelm
more elementary pgiptype;
2013-05-14, by wenzelm
prefer Markup.parse/print operations -- slight change of exception behaviour;
2013-05-14, by wenzelm
more uniform Markup.print_real;
2013-05-14, by wenzelm
removed dead code;
2013-05-14, by wenzelm
more uniform Markup.parse_real;
2013-05-14, by wenzelm
tuned signature;
2013-05-14, by wenzelm
more robust load_timings: ignore JVM errors such as java.lang.OutOfMemoryError;
2013-05-14, by wenzelm
tuned;
2013-05-14, by wenzelm
misc tuning and simplification;
2013-05-14, by wenzelm
more frugal line termination, to cope with huge log files (see also 016cb7d8f297);
2013-05-14, by wenzelm
more scalable File.write via separate chunks;
2013-05-14, by wenzelm
more scalable Library.separate -- NB: JVM has tiny fixed-size stack;
2013-05-14, by wenzelm
support for more informative crashes;
2013-05-14, by wenzelm
more antiquotations;
2013-05-14, by wenzelm
tuned messages;
2013-05-14, by wenzelm
more generous java resources via ISABELLE_BUILD_JAVA_OPTIONS;
2013-05-14, by wenzelm
generate valid direct Isar proof also if the facts are contradictory
2013-05-14, by blanchet
tuned names
2013-05-14, by nipkow
tuned names
2013-05-14, by nipkow
removed obsolete PGIP material;
2013-05-13, by wenzelm
more direct output of remaining PGIP rudiments;
2013-05-13, by wenzelm
simplified preferences, removed obsolete operations;
2013-05-13, by wenzelm
tuned signature;
2013-05-13, by wenzelm
more direct output of remaining PGIP rudiments;
2013-05-13, by wenzelm
obsolete;
2013-05-13, by wenzelm
removed obsolete PGIP material;
2013-05-13, by wenzelm
recovered informative progress from 016cb7d8f297;
2013-05-13, by wenzelm
removed obsolete PGIP material;
2013-05-13, by wenzelm
clean startup of RAW session;
2013-05-13, by wenzelm
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

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

isabelle