isabelle: Graph

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

parse agsyHOL proofs (as unsat cores)
2013-05-20, by blanchet
freeze types in Sledgehammer goal, not just terms
2013-05-20, by blanchet
generate agsyHOL-friendly THF (to some extent -- partial application of connectives remains an issue)
2013-05-20, by blanchet
tuned code
2013-05-20, by blanchet
started adding agsyHOL as an experimental prover
2013-05-20, by blanchet
defined lvars and rvars of commands separately.
2013-05-20, by nipkow
made "completish" mode a bit more complete
2013-05-19, by blanchet
infrastructure for generic data for code symbols (constants, type constructors, classes, instances)
2013-05-19, by haftmann
tuned and clarified
2013-05-19, by haftmann
tuned, including signature
2013-05-19, by haftmann
discontinued odd workaround for scala-2.10.0-RC1;
2013-05-18, by wenzelm
discontinued odd workaround for scala-2.9.2, which is hopefully obsolete in scala-2.10.x;
2013-05-18, by wenzelm
explicit notion of public options, which are shown in the editor options dialog;
2013-05-18, by wenzelm
back to more paranoid interrupt test after request is cancelled -- avoid race condition;
2013-05-17, by wenzelm
timeout counts as regular error, with rc = 1 (cf. special Exn.Interrupt vs. regular TimeLimit.TimeOut in Isabelle/ML);
2013-05-17, by wenzelm
added isabelle tty option -o;
2013-05-17, by wenzelm
oops;
2013-05-17, by wenzelm
renamed 'print_configs' to 'print_options';
2013-05-17, by wenzelm
proper option quick_and_dirty;
2013-05-17, by wenzelm
retain quick_and_dirty as-is -- no censorship;
2013-05-17, by wenzelm
more system-atic options;
2013-05-17, by wenzelm
added isabelle-process option -o;
2013-05-17, by wenzelm
more precise "eval", cf. isabelle build;
2013-05-17, by wenzelm
discontinued obsolete isabelle-process options -f and -u;
2013-05-17, by wenzelm
NEWS;
2013-05-17, by wenzelm
discontinued obsolete isabelle usedir, mkdir, make;
2013-05-17, by wenzelm
modernized TimeLimit.timeLimit using Event_Timer service -- based on more elementary version 11ae688e4e30;
2013-05-17, by wenzelm
event timer as separate service thread;
2013-05-17, by wenzelm
tuned signature;
2013-05-17, by wenzelm
tuned signature -- emphasize thread creation here;
2013-05-17, by wenzelm
repair after bc01725d7918;
2013-05-17, by wenzelm
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
2013-05-17, by nipkow
tuned
2013-05-17, by nipkow
merged
2013-05-16, by wenzelm
more system options as context-sensitive config options;
2013-05-16, by wenzelm
Thy_Output.modes as proper option;
2013-05-16, by wenzelm
some system options as context-sensitive config options;
2013-05-16, by wenzelm
system options as context-sensitive configuration options within the attribute name space;
2013-05-16, by wenzelm
tuned signature;
2013-05-16, by wenzelm
properly handle SPASS constructors w.r.t. partially applied functions
2013-05-16, by blanchet
tuned signature -- depend on context by default;
2013-05-16, by wenzelm
reflexivity rules for the function type and equality
2013-05-16, by kuncar
tuned comments
2013-05-16, by blanchet
correctly 'repair' the monomorphization context for SMT solvers from Sledgehammer
2013-05-16, by blanchet
tuning
2013-05-16, by blanchet
more work on SPASS datatypes
2013-05-16, by blanchet
tuning -- renamed '_from_' to '_of_' in Sledgehammer
2013-05-16, by blanchet
compile
2013-05-16, by blanchet
don't recognize overloaded constants as constructors for the purpose of removing type arguments
2013-05-16, by blanchet
tuning
2013-05-16, by blanchet
reintroduced syntax for "nonexhaustive" datatypes
2013-05-16, by blanchet
tuning
2013-05-16, by blanchet
more work on SPASS datatypes
2013-05-16, by blanchet
merged
2013-05-16, by Andreas Lochbihler
setup for set membership as a predicate for code_pred
2013-05-16, by Andreas Lochbihler
tuned
2013-05-16, by nipkow
explicitly state equivalence relation for sim; tweak syntax of sem_equiv
2013-05-16, by kleing
merged
2013-05-16, by nipkow
finally: acom with pointwise access and update of annotations
2013-05-16, by nipkow
merged;
2013-05-15, by wenzelm
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