isabelle: Graph

Theorem "arctan" is no longer a default simprule
2015-04-01, by paulson
John Harrison's example: a 32-bit approximation to pi. SLOW
2015-04-01, by paulson
HOL Light Libraries for complex Arctan, Arcsin, Arccos
2015-04-01, by paulson
arcsin and arccos lemmas
2015-04-01, by paulson
NEWS
2015-03-31, by haftmann
given up separate type classes demanding `inverse 0 = 0`
2015-03-31, by haftmann
Merge
2015-03-31, by paulson
rationalised and generalised some theorems concerning abs and x^2.
2015-03-31, by paulson
added lemmas
2015-03-31, by nipkow
Merge
2015-03-31, by paulson
New material and binomial fix
2015-03-31, by paulson
tuned doc
2015-03-31, by blanchet
merged
2015-03-31, by wenzelm
tuned signature;
2015-03-31, by wenzelm
support for strictly private name space entries;
2015-03-30, by wenzelm
tuned signature;
2015-03-30, by wenzelm
export more low-level theorems in data structure (partly for 'corec')
2015-03-30, by blanchet
tuned;
2015-03-30, by wenzelm
merged
2015-03-30, by wenzelm
more uniform syntax for named instantiations;
2015-03-30, by wenzelm
merged
2015-03-30, by hoelzl
added locale for semirings
2015-03-30, by Rene Thiemann
exposed approximation in ML
2015-03-30, by eberlm
clarified NEWS (cf. 97872c658a44);
2015-03-30, by wenzelm
clarified equality of formal entities;
2015-03-29, by wenzelm
merged
2015-03-29, by wenzelm
tuned signature;
2015-03-29, by wenzelm
ind_cases: clarified preparation of arguments;
2015-03-29, by wenzelm
support for minimal specifications, with usual treatment of fixes and dummies;
2015-03-29, by wenzelm
tuned;
2015-03-29, by wenzelm
tuned;
2015-03-29, by wenzelm
tuned signature;
2015-03-29, by wenzelm
proper local Proof_Context.arity_sorts;
2015-03-29, by wenzelm
more standard Sign.typ_match: sorts should be alright in result of Syntax.check_terms;
2015-03-29, by wenzelm
avoid low-level tsig operations;
2015-03-29, by wenzelm
tuned;
2015-03-29, by wenzelm
clarified context;
2015-03-29, by wenzelm
rule_insts_schematic is considered legacy and false by default;
2015-03-29, by wenzelm
tuned;
2015-03-29, by wenzelm
clarified no_zero_devisors: makes only sense in a semiring;
2015-03-28, by haftmann
dropped long-outdated comments
2015-03-28, by haftmann
merged
2015-03-28, by wenzelm
clarified goal context;
2015-03-28, by wenzelm
clarified goal context;
2015-03-28, by wenzelm
prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;
2015-03-28, by wenzelm
proper Rule_Insts.read_term, e.g. to enable case_tac using "_";
2015-03-27, by wenzelm
tuned signature;
2015-03-27, by wenzelm
clarified goal context;
2015-03-27, by wenzelm
clarified doc
2015-03-27, by blanchet
more graceful failure if some of the involved BNFs have no data
2015-03-27, by blanchet
sort BNFs in output
2015-03-27, by blanchet
preserve order of type arguments in pre-FP BNF typedef
2015-03-27, by blanchet
register pre-fixpoint BNFs in database to enable lookup later (e.g. in 'corec')
2015-03-26, by blanchet
store low-level (un)fold constants
2015-03-26, by blanchet
export more functions
2015-03-26, by blanchet
restored broken metis proof
2015-03-26, by haftmann
distributivity of partial minus establishes desired properties of dvd in semirings
2015-03-23, by haftmann
explicit commutative additive inverse operation;
2015-03-23, by haftmann
modernized
2015-03-23, by haftmann
more multiset theorems
2015-03-25, by blanchet
semantic completion for @{system_option};
2015-03-25, by wenzelm
clarified position;
2015-03-25, by wenzelm
HOL-SPARK .prv files are subject to system option spark_prv;
2015-03-25, by wenzelm
tuned signature;
2015-03-25, by wenzelm
NEWS;
2015-03-25, by wenzelm
prefer local fixes;
2015-03-25, by wenzelm
proper signature;
2015-03-25, by wenzelm
dummies may depend on goal params as well;
2015-03-25, by wenzelm
merged
2015-03-24, by wenzelm
proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;
2015-03-24, by wenzelm
clarified case_tac fixes and context;
2015-03-24, by wenzelm
clarified name;
2015-03-24, by wenzelm
option to control old-style schematic mode;
2015-03-24, by wenzelm
clarified role of Name.uu_, which happens to be the internal replacement of the first underscore under certain assumptions about the context;
2015-03-24, by wenzelm
tuned;
2015-03-24, by wenzelm
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