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 +30000 tip

merged
2010-09-20, by wenzelm
merged
2010-09-20, by haftmann
more accurate exception handling
2010-09-20, by haftmann
merged
2010-09-20, by blanchet
merge tracing of two related modules
2010-09-20, by blanchet
merged
2010-09-20, by blanchet
preprocess "All" before doing clausification in Metis;
2010-09-18, by blanchet
reorder proof methods and take out "best";
2010-09-17, by blanchet
renaming variable name to decrease likelyhood of nameclash
2010-09-20, by bulwahn
code_pred_intro can be used to name facts for the code_pred command
2010-09-20, by bulwahn
replacing temporary hack by checking for environment settings of the component
2010-09-20, by bulwahn
removing unnessary options for code_pred
2010-09-20, by bulwahn
moving renaming_vars to post_processing; removing clone in values and quickcheck of code_prolog
2010-09-20, by bulwahn
removing clone in code_prolog and predicate_compile_quickcheck
2010-09-20, by bulwahn
adjusted
2010-09-20, by haftmann
updated file duplicate
2010-09-20, by haftmann
\\isatypewrite now part of isabelle latex style
2010-09-20, by haftmann
made smlnj happy
2010-09-20, by haftmann
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
2010-09-19, by boehmes
do not treat natural numbers as a datatype (natural numbers are considered an abstract type with a coercion to integers)
2010-09-19, by boehmes
generalized lemma insort_remove1 to insort_key_remove1
2010-09-17, by haftmann
generalized lemmas multiset_of_insort, multiset_of_sort, properties_for_sort for *_key variants
2010-09-17, by haftmann
merged
2010-09-17, by haftmann
less intermediate data structures
2010-09-17, by haftmann
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
2010-09-20, by wenzelm
simplified Isabelle_System.mk_fifo: inlined script, append PPID and PID uniformly;
2010-09-19, by wenzelm
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
2010-09-19, by wenzelm
back to default fold painter -- Circle looks slightly odd in conjunction with bracket matching;
2010-09-19, by wenzelm
message_actor: more robust treatment of EOF;
2010-09-19, by wenzelm
simplified Isabelle_Process message kinds;
2010-09-19, by wenzelm
recovered basic session stop/restart;
2010-09-18, by wenzelm
simplified fifo handling -- rm_fifo always succeeds without ever blocking;
2010-09-18, by wenzelm
raw_execute: let IOException pass-through unhindered (again);
2010-09-18, by wenzelm
mkfifo: some workaround to ensure reasonably unique id, even on Cygwin where $PPID might fall back on odd default;
2010-09-18, by wenzelm
Isabelle_System.mk_fifo: more robust enumeration of unique names, based on persisting JVM pid (parent of shell process);
2010-09-18, by wenzelm
slightly more robust Isabelle_Process startup -- NB: openening fifo streams synchronizes with other end, which may fail to reach that point;
2010-09-18, by wenzelm
tuned;
2010-09-18, by wenzelm
separate Isabelle.logic_selector;
2010-09-18, by wenzelm
non-editable text area;
2010-09-18, by wenzelm
basic setup for prover session panel;
2010-09-18, by wenzelm
ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
2010-09-17, by wenzelm
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
2010-09-17, by wenzelm
Isabelle_Markup.overview_color: indicate error / warning messages;
2010-09-17, by wenzelm
some specific message classification;
2010-09-17, by wenzelm
Syntax.read_asts error: report token ranges within message -- no side-effect here;
2010-09-17, by wenzelm
Isabelle_Process: status/report do not require serial numbers;
2010-09-17, by wenzelm
simplified some internal flags using Config.T instead of full-blown Proof_Data;
2010-09-17, by wenzelm
tuned signature of (Context_)Position.report variants;
2010-09-17, by wenzelm
merged
2010-09-17, by wenzelm
merged
2010-09-17, by blanchet
update README
2010-09-17, by blanchet
regenerate "metis.ML"
2010-09-17, by blanchet
fix license
2010-09-17, by blanchet
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
2010-09-17, by blanchet
move functions around
2010-09-17, by blanchet
simplify Skolem handling;
2010-09-17, by blanchet
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
2010-09-17, by blanchet
complete refactoring of Metis along the lines of Sledgehammer
2010-09-16, by blanchet
got caught once again by SML's pattern maching (ctor vs. var)
2010-09-16, by blanchet
added new "Metis_Reconstruct" module, temporarily empty
2010-09-16, by blanchet

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

isabelle