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

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