Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
proper context;
2015-03-06, by wenzelm
tuned;
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
updated to scala-2.11.6;
2015-03-06, by wenzelm
Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-06, by wenzelm
merged
2015-03-06, by wenzelm
merged
2015-03-06, by wenzelm
clarified context;
2015-03-06, by wenzelm
tuned -- more explicit use of context;
2015-03-06, by wenzelm
tuned -- more explicit use of context;
2015-03-05, by wenzelm
A few new lemmas and a bit of tidying up
2015-03-06, by paulson
Merge
2015-03-05, by paulson
The function frac. Various lemmas about limits, series, the exp function, etc.
2015-03-05, by paulson
avoid needless 'if ... undefined' in generated theorems
2015-03-05, by blanchet
strengthened tactic
2015-03-05, by blanchet
strengthened tactic
2015-03-05, by blanchet
deal better with corecursion through functions
2015-03-05, by blanchet
removed too strict checks
2015-03-05, by blanchet
message tuning
2015-03-05, by blanchet
tuning
2015-03-05, by blanchet
improved primcorec messages
2015-03-05, by blanchet
improved primcorec messages
2015-03-05, by blanchet
better primcorec messages
2015-03-05, by blanchet
more primcorec messages
2015-03-05, by blanchet
more precise primcorec messages
2015-03-05, by blanchet
more precise primcorec messages
2015-03-05, by blanchet
better primcorec messages
2015-03-05, by blanchet
more 'primcorec' error handling
2015-03-05, by blanchet
helpful error message when 'auto' fails
2015-03-05, by blanchet
no quick_and_dirty for goals that may fail + tuned messages
2015-03-05, by blanchet
tuned new primrec messages
2015-03-05, by blanchet
reworked primcorec error messages
2015-03-05, by blanchet
fix import path
2015-03-05, by hoelzl
merged
2015-03-04, by wenzelm
tuned signature;
2015-03-04, by wenzelm
tuned signature;
2015-03-04, by wenzelm
removed unused;
2015-03-04, by wenzelm
merged
2015-03-04, by nipkow
Removed the obsolete functions "natfloor" and "natceiling"
2015-03-04, by nipkow
clarified signature;
2015-03-04, by wenzelm
tuned;
2015-03-04, by wenzelm
tuned;
2015-03-04, by wenzelm
merged;
2015-03-04, by wenzelm
tuned signature -- prefer qualified names;
2015-03-04, by wenzelm
alist is a BNF
2015-03-04, by traytel
eliminated some clones of Proof_Context.cterm_of
2015-03-03, by traytel
updated docs
2015-03-03, by blanchet
strengthened 'size' tactic for examples like datatype (dead 'a, 'b) y = Y "'a * 'b"
2015-03-03, by blanchet
SPASS-Pirate is now called Pirate
2015-03-03, by blanchet
avoid duplicate simp warning for datatypes with explicit products
2015-03-03, by blanchet
removed needless (and inconsistent) qualifier that messes up with Mirabelle
2015-03-03, by blanchet
import 'Main' to be on the safe side
2015-03-03, by blanchet
added Proof_Context.cterm_of/ctyp_of convenience;
2015-03-01, by wenzelm
tuned;
2015-03-01, by wenzelm
updated to jedit-5.2.0;
2015-02-28, by wenzelm
spelling
2015-02-28, by haftmann
tuned whitespace;
2015-02-27, by wenzelm
typo
2015-02-26, by nipkow
tuned;
2015-02-24, by wenzelm
updated CVC4 component to include libgmp on Mac OS X
2015-02-24, by blanchet
more uniform headless mode for all derivatives of "build" (amending df5dc24ca712);
2015-02-23, by wenzelm
Goal.prove_multi is superseded by the fully general Goal.prove_common;
2015-02-23, by wenzelm
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
support for off-line graph output, without GUI thread;
2015-01-25, by wenzelm
make it independent from GUI thread, e.g. for Graph_File.write;
2015-01-25, by wenzelm
separate module Graph_File;
2015-01-25, by wenzelm
tuned comments;
2015-01-25, by wenzelm
tuned;
2015-01-25, by wenzelm
more compact message;
2015-01-25, by wenzelm
proper naming convention;
2015-01-25, by wenzelm
prefer plain tuples;
2015-01-25, by wenzelm
tuned message;
2015-01-25, by wenzelm
tuned;
2015-01-25, by wenzelm
tuned signature;
2015-01-24, by wenzelm
tuned;
2015-01-24, by wenzelm
tuned message;
2015-01-24, by wenzelm
more direct Output.output;
2015-01-24, by wenzelm
avoid newline in Pretty.str;
2015-01-24, by wenzelm
merged
2015-01-23, by Andreas Lochbihler
generalise lemma
2015-01-23, by Andreas Lochbihler
integral of the product of count spaces equals the integral of the count space of the product type
2015-01-23, by hoelzl
import general thms from Density_Compiler
2015-01-22, by hoelzl
backout cefeea956989: Graphview *is* required in Pure to replace old browser eventually;
2015-01-22, by wenzelm
backed out obsolete workaround from ef1edfb36af7
2015-01-22, by haftmann
disjunctive bottom and supremum lists
2015-01-21, by haftmann
sufficent to have graphview as part of jEdit rather than Pure
2015-01-21, by haftmann
option for formally inlined class specifications in hierarchy graph
2015-01-21, by haftmann
clarified iterations: enforce full top_down/bottom_up cycle for better stability of layout;
2015-01-21, by wenzelm
updated to jdk-7u76, which appears to be more stable than jdk-8u31 (e.g. crashes jEdit/Console plugin of Mac OS X);
2015-01-21, by wenzelm
updated jdk-8u31;
2015-01-21, by wenzelm
generalized sum_diff_distrib to setsum_subtractf_nat
2015-01-20, by hoelzl
tuned measurability proofs
2015-01-16, by hoelzl
typo in description
2015-01-19, by blanchet
tuned message;
2015-01-19, by wenzelm
always swap panels, which leads to slightly better GUI layout;
2015-01-19, by wenzelm
suppress inactive controls (again);
2015-01-19, by wenzelm
tuned colors;
2015-01-19, by wenzelm
tuned;
2015-01-19, by wenzelm
more symmetric layout of main panel;
2015-01-19, by wenzelm
clarified edge_color;
2015-01-19, by wenzelm
proper tooltips -- override action toolTip which is empty here;
2015-01-19, by wenzelm
no document here;
2015-01-19, by wenzelm
discontinued attempt at alphabetic_order -- selection via regex should be sufficient;
2015-01-18, by wenzelm
suppress some controls that don't work yet;
2015-01-18, by wenzelm
proper selection of nodes via regular expression;
2015-01-18, by wenzelm
obsolete -- full layout takes approx. 100ms;
2015-01-18, by wenzelm
suppress some controls that don't work yet;
2015-01-18, by wenzelm
tuned;
2015-01-18, by wenzelm
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
tip