isabelle: Graph

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
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