isabelle: Graph

tuned proof;
2015-03-24, by wenzelm
admit dummy patterns in instantiations;
2015-03-24, by wenzelm
clarified input source;
2015-03-24, by wenzelm
tuning
2015-03-24, by blanchet
reordered properties
2015-03-24, by blanchet
NEWS;
2015-03-23, by wenzelm
tuned proof;
2015-03-23, by wenzelm
implicit goal parameters are improper;
2015-03-23, by wenzelm
merged
2015-03-23, by wenzelm
prefer local fixes;
2015-03-23, by wenzelm
local fixes may depend on goal params;
2015-03-23, by wenzelm
tuned;
2015-03-23, by wenzelm
clarified syntax category "fixes";
2015-03-23, by wenzelm
tuned signature;
2015-03-23, by wenzelm
tuned syntax diagrams -- no duplication of "target";
2015-03-23, by wenzelm
tuned;
2015-03-23, by wenzelm
tuned;
2015-03-23, by wenzelm
support 'for' fixes in rule_tac etc.;
2015-03-23, by wenzelm
fix parameter order of NO_MATCH
2015-03-23, by hoelzl
add measurable_submarkov
2015-03-23, by hoelzl
BT subsumed by Library/Tree
2015-03-23, by nipkow
added funs and lemmas
2015-03-23, by nipkow
tuned;
2015-03-22, by wenzelm
tuned;
2015-03-22, by wenzelm
tuned;
2015-03-22, by wenzelm
tuned;
2015-03-20, by wenzelm
read instantiations uniformly for rules and tactics;
2015-03-20, by wenzelm
removed presumably pointless detail;
2015-03-20, by wenzelm
tuned;
2015-03-20, by wenzelm
tuned;
2015-03-20, by wenzelm
make SML/NJ happy;
2015-03-20, by wenzelm
Merge
2015-03-20, by paulson
tweaked a few slow or very ugly proofs
2015-03-20, by paulson
merged
2015-03-20, by wenzelm
tuned signature;
2015-03-20, by wenzelm
tuned;
2015-03-20, by wenzelm
tuned signature;
2015-03-20, by wenzelm
tuned;
2015-03-20, by wenzelm
tuned -- prepare instantiation more uniformly;
2015-03-20, by wenzelm
Merge
2015-03-20, by paulson
fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!
2015-03-20, by paulson
merged
2015-03-19, by wenzelm
more position information;
2015-03-19, by wenzelm
misc tuning;
2015-03-19, by wenzelm
tuned;
2015-03-19, by wenzelm
Merge
2015-03-19, by paulson
New material for complex sin, cos, tan, Ln, also some reorganisation
2015-03-19, by paulson
updated to sumatra_pdf-3.0;
2015-03-19, by wenzelm
tuned comments;
2015-03-19, by wenzelm
slightly more formal historic examples;
2015-03-19, by wenzelm
bounded powerset
2015-03-18, by traytel
new HOL Light material about exp, sin, cos
2015-03-18, by paulson
new file for complex transcendental functions
2015-03-18, by paulson
Merge
2015-03-18, by paulson
Merge
2015-03-18, by paulson
Merge
2015-03-18, by paulson
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
2015-03-18, by paulson
merged
2015-03-18, by noschinl
added proof method rewrite
2015-03-18, by noschinl
merged
2015-03-18, by wenzelm
tuned;
2015-03-17, by wenzelm
tight span for theory header, which is relevant for error positions (including semantic completion);
2015-03-17, by wenzelm
misc tuning and simplification;
2015-03-17, by wenzelm
Inserted real_of_nat to fix factorial-related problem
2015-03-17, by paulson
more general type class for factorial. Now allows code generation (?)
2015-03-17, by paulson
Merge
2015-03-17, by paulson
Merge
2015-03-17, by paulson
The factorial function, "fact", now has type "nat => 'a"
2015-03-16, by paulson
merged
2015-03-17, by nipkow
added lemmas
2015-03-17, by nipkow
document property
2015-03-16, by traytel
BNF relators preserve reflexivity
2015-03-16, by traytel
export more ML functions
2015-03-16, by blanchet
merged
2015-03-16, by wenzelm
suppress semantic completion in errors of batch build -- avoid junk in log files;
2015-03-16, by wenzelm
updated docs
2015-03-16, by blanchet
clarified documentation
2015-03-16, by blanchet
proper headers;
2015-03-16, by wenzelm
merged
2015-03-16, by wenzelm
tuned message -- include completion;
2015-03-16, by wenzelm
support for completion reports produced in Scala (inlined into messages);
2015-03-16, by wenzelm
more precises positions;
2015-03-16, by wenzelm
avoid duplicate header errors, more precise positions;
2015-03-16, by wenzelm
tuned protocol -- resolve command positions in ML;
2015-03-16, by wenzelm
clarified modules;
2015-03-16, by wenzelm
add inequalities (move from AFP/Amortized_Complexity)
2015-03-16, by hoelzl
merge
2015-03-15, by blanchet
inlining threshold
2015-03-15, by blanchet
avoid controversial Pirate syntax
2015-03-15, by blanchet
more markup, which helps to create missing imports;
2015-03-15, by wenzelm
tuned signature;
2015-03-15, by wenzelm
proper command id for inlined errors, which is important for Command.State.accumulate;
2015-03-15, by wenzelm
clarified span position;
2015-03-15, by wenzelm
tuned;
2015-03-15, by wenzelm
tuned;
2015-03-15, by wenzelm
hybrid use of command blobs: inlined errors and auxiliary files;
2015-03-15, by wenzelm
more command categories, as in ML;
2015-03-15, by wenzelm
more command categories, as in ML;
2015-03-15, by wenzelm
tuned;
2015-03-15, by wenzelm
value-oriented user error, for well-defined Thy_Syntax.chop_common;
2015-03-14, by wenzelm
more explicit exception User_Error, with value-oriented equality;
2015-03-14, by wenzelm
tuned signature;
2015-03-14, by wenzelm
clarified positions of theory imports;
2015-03-14, by wenzelm
misc tuning -- more uniform ML vs. Scala;
2015-03-14, by wenzelm
tunes signature -- more uniform ML vs. Scala;
2015-03-14, by wenzelm
position parser as in ML;
2015-03-14, by wenzelm
tuned signature;
2015-03-13, by wenzelm
rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed
2015-03-13, by nipkow
simplified Command.resolve_files in ML, using blobs_index from Scala;
2015-03-13, by wenzelm
removed junk;
2015-03-13, by wenzelm
tuned;
2015-03-13, by wenzelm
merged
2015-03-12, by wenzelm
clarified markup for embedded files, early before execution;
2015-03-12, by wenzelm
clarified command content;
2015-03-12, by wenzelm
tuned -- more uniform ML vs. Scala;
2015-03-12, by wenzelm
quote "method" to allow Eisbach using this keyword;
2015-03-12, by wenzelm
rel_pmf on equivalence relation
2015-03-12, by hoelzl
make proofs work with 4762c690a75c
2015-03-12, by Andreas Lochbihler
add subadditivity for Liminf on ereal
2015-03-11, by hoelzl
merged
2015-03-11, by Andreas Lochbihler
merged
2015-03-10, by Andreas Lochbihler
more type class instances
2015-03-10, by Andreas Lochbihler
documented renamed theories
2015-03-10, by blanchet
export more functions (for future 'corec')
2015-03-10, by blanchet
tuning
2015-03-10, by blanchet
merged
2015-03-10, by wenzelm
more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
2015-03-10, by wenzelm
generalized bind_cond_pmf_cancel
2015-03-10, by hoelzl
renaming HOL/Fact.thy -> Binomial.thy
2015-03-10, by paulson
Merge
2015-03-10, by paulson
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2015-03-10, by paulson
clarified Token.check_src: intern at most once;
2015-03-10, by wenzelm
add set_pmf lemmas to simpset
2015-03-10, by hoelzl
build pmf's on bind
2015-03-10, by hoelzl
split into subgoals
2015-03-10, by blanchet
tuning
2015-03-10, by blanchet
merged
2015-03-09, by wenzelm
support structural composition (THEN_ALL_NEW) for proof methods;
2015-03-09, by wenzelm
Removed the infix operator "choose" to allow HOLCF to build
2015-03-09, by paulson
sin, cos generalised from type real to any "'a::{real_normed_field,banach}", including complex
2015-03-09, by paulson
eliminated unused arith "verbose" flag -- tools that need options can use the context;
2015-03-09, by wenzelm
eliminated dead code (cf. 5e5c36b051af);
2015-03-09, by wenzelm
tuned;
2015-03-09, by wenzelm
clarified aliases;
2015-03-08, by wenzelm
misc tuning and simplification;
2015-03-08, by wenzelm
tuned;
2015-03-08, by wenzelm
misc tuning and simplification;
2015-03-08, by wenzelm
tuned;
2015-03-08, by wenzelm
cartouche_declaration for Eisbach;
2015-03-08, by wenzelm
NEWS;
2015-03-07, by wenzelm
clarified Drule.gen_all: observe context more carefully;
2015-03-07, by wenzelm
added declare_maxidx operations for Eisbach;
2015-03-07, by wenzelm
clarified Variable.export: observe maxidx of target context;
2015-03-07, by wenzelm
tuned;
2015-03-07, 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
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