isabelle: Graph

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

proper LaTeX;
2015-02-23, by wenzelm
make SML/NJ more happy;
2015-02-23, by wenzelm
added new tree material
2015-02-21, by nipkow
generalised the results by Eberl
2015-02-20, by paulson
more canonical order of subscriptions avoids superfluous facts
2015-02-19, by haftmann
got rid of linordered_field_class.sign_simps(41) !
2015-02-19, by paulson
establish unique preferred fact names
2015-02-19, by haftmann
eliminated technical fact alias
2015-02-18, by haftmann
eliminated fact duplicates
2015-02-18, by haftmann
inlined rules to free user-space from technical names
2015-02-18, by haftmann
explicit declaration allows cumulative declaration
2015-02-18, by haftmann
use more permissive logic for CVC4 (in case both reals and datatypes appear)
2015-02-17, by blanchet
deleted ineffective declarations
2015-02-15, by haftmann
dropped unused rules
2015-02-15, by haftmann
more direct expression of syntactic function records
2015-02-15, by haftmann
self-contained declaration attribute
2015-02-15, by haftmann
simpset with no redundancy
2015-02-15, by haftmann
times_divide_eq rules are already [simp] despite of comment
2015-02-15, by haftmann
explicit equivalence for strict order on lattices
2015-02-15, by haftmann
tuned
2015-02-15, by haftmann
purge variables not mentioned in body from pattern
2015-02-15, by haftmann
only collapse patterns with disjunctive variable names
2015-02-14, by haftmann
clarified
2015-02-14, by haftmann
avoid unused arguments
2015-02-14, by haftmann
tuned
2015-02-14, by haftmann
more consistent teminology
2015-02-14, by haftmann
fact consolidation
2015-02-14, by haftmann
dropped redundancy
2015-02-14, by haftmann
less warnings
2015-02-14, by haftmann
merged
2015-02-13, by wenzelm
proper context;
2015-02-11, by wenzelm
proper context;
2015-02-11, by wenzelm
proper context;
2015-02-11, by wenzelm
proper context;
2015-02-11, by wenzelm
proper context and method setup;
2015-02-11, by wenzelm
new lemmas re refinement of one equivalence relation WRT another
2015-02-12, by paulson
rel_pmf preserves orders
2015-02-11, by Andreas Lochbihler
generalise lemma
2015-02-11, by Andreas Lochbihler
more lemmas
2015-02-11, by Andreas Lochbihler
merged
2015-02-11, by Andreas Lochbihler
more transfer rules
2015-02-11, by Andreas Lochbihler
add lemmas about functions on option
2015-02-11, by Andreas Lochbihler
tuned proof
2015-02-11, by Andreas Lochbihler
add lema about card and vimage
2015-02-11, by Andreas Lochbihler
add more general version of finite_vimageD
2015-02-11, by Andreas Lochbihler
add lemma
2015-02-11, by Andreas Lochbihler
add lemmas about flat_ord
2015-02-11, by Andreas Lochbihler
add parametricity rules for monotone, fun_lub, and fun_ord
2015-02-11, by Andreas Lochbihler
add parametricity rule for Ex1
2015-02-11, by Andreas Lochbihler
add intro and elim rules for right_total
2015-02-11, by Andreas Lochbihler
add monotonicity lemmas for rel_fun
2015-02-11, by Andreas Lochbihler
add lemmas about bind and image
2015-02-11, by Andreas Lochbihler
updated NEWS
2015-02-11, by blanchet
updated Sledgehammer docs
2015-02-11, by blanchet
added CVC4 component (and took out CVC3 from main components)
2015-02-11, by blanchet
tuned default provers
2015-02-11, by blanchet
Merge
2015-02-11, by paulson
Not a simprule, as it complicates proofs
2015-02-10, by paulson
Merge
2015-02-10, by paulson
New lemmas and a bit of tidying up.
2015-02-10, by paulson
check unused theory;
2015-02-10, by wenzelm
tuned;
2015-02-10, by wenzelm
more accurate context;
2015-02-10, by wenzelm
merged
2015-02-10, by wenzelm
misc tuning;
2015-02-10, by wenzelm
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
2015-02-10, by wenzelm
indicate slow proof (approx. 20s);
2015-02-10, by wenzelm
merged
2015-02-10, by hoelzl
add bind_cond_pmf_cancel
2015-02-10, by hoelzl
add cond_map_pmf
2015-02-10, by hoelzl
introduce discrete conditional probabilities, use it to simplify bnf proof of pmf
2015-02-10, by hoelzl
tuned proof
2015-02-10, by Andreas Lochbihler
add another lemma to split nn_integral over product count_space
2015-02-10, by Andreas Lochbihler
tune proof
2015-02-10, by Andreas Lochbihler
nn_integral can be split over arbitrary product count_spaces
2015-02-10, by Andreas Lochbihler
add stronger version of lemma
2015-02-10, by Andreas Lochbihler
default abstypes and default abstract equations make technical (no_code) annotation superfluous
2015-02-06, by haftmann
careful about visibility of facts that have the same 'theory' in optimization
2015-02-06, by blanchet
non-intrusive default code setup for mappings
2015-02-06, by haftmann
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
2015-02-05, by haftmann
explicit type annotation avoids problems with Haskell type inference
2015-02-05, by haftmann
more explicit hint on import order
2015-02-05, by haftmann
dropped dead code;
2015-02-05, by haftmann
dropped obsolete external entrance point
2015-02-05, by haftmann
explicit error message for non-existing targets
2015-02-05, by haftmann
fixed typos
2015-02-02, by blanchet
less confusing constant
2015-02-02, by blanchet
tuning
2015-02-02, by blanchet
simp rules for return_pmf
2015-01-30, by hoelzl
related permutations with bij functions
2015-01-30, by hoelzl
canonical name
2015-01-30, by nipkow
discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;
2015-01-29, by wenzelm
more explicit indication of Async_Manager_Legacy as Proof General legacy;
2015-01-29, by wenzelm
tuned bootstrap;
2015-01-29, by wenzelm
tuned;
2015-01-29, by wenzelm
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
2015-01-29, by wenzelm
unused;
2015-01-29, by wenzelm
ensure that running into older execution is interruptible (see also b91dc7ab3464);
2015-01-29, by wenzelm
clarified worker_wait;
2015-01-29, by wenzelm
explicit headless mode for machines that lack X11 (e.g. lxbroy10);
2015-01-28, by wenzelm
more robust protocol command: purge removed execs asynchronously, to remain reactive despite problems to cancel "Command.run_process" in a situation of overrunning non-terminating tasks (see also 59f1591a11cb);
2015-01-28, by wenzelm
tuned signature;
2015-01-28, by wenzelm
tuned comment;
2015-01-28, by wenzelm
tuned signature;
2015-01-28, by wenzelm
clarified module name;
2015-01-28, by wenzelm
abstract code equation may also be default
2015-01-28, by haftmann
proper term_of for iarray
2015-01-28, by haftmann
string printing conformant to both (S)ML and Isabelle/ML
2015-01-28, by haftmann
Fixed bug in bugfix for function package
2015-01-28, by eberlm
Fixed variable naming bug in function package
2015-01-28, by eberlm
moved bcontfun from AFP/Ordinary_Differential_Equations
2015-01-28, by hoelzl
ereal: tuned proofs concerning continuity and suprema
2015-01-27, by hoelzl
spelling error
2015-01-26, by hoelzl
NEWS;
2015-01-26, by wenzelm
removed unused operations;
2015-01-26, by wenzelm
prefer plain session_graph.pdf over GraphBrowser applet;
2015-01-26, by wenzelm
complete pattern coverage, e.g. relevant for singleton graph;
2015-01-26, by wenzelm
discontinued obsolete option "document_graph";
2015-01-25, by wenzelm
provide session_graph.pdf via Isabelle/Scala;
2015-01-25, by wenzelm
support for session graph from Scala side;
2015-01-25, by wenzelm