2016-08-02 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
2016-08-02 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
2016-08-01 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
2016-07-29 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|
2016-07-08 |
haftmann |
avoid to hide equality behind (output) abbreviation
|
file |
diff |
annotate
|
2016-07-05 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
2016-07-02 |
haftmann |
more theorems
|
file |
diff |
annotate
|
2016-06-20 |
wenzelm |
prefer HOL definitions;
|
file |
diff |
annotate
|
2016-06-20 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
2016-06-20 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
2016-05-09 |
paulson |
renamings and refinements
|
file |
diff |
annotate
|
2016-04-04 |
paulson |
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
|
file |
diff |
annotate
|
2016-03-14 |
paulson |
Refactoring (moving theorems into better locations), plus a bit of new material
|
file |
diff |
annotate
|
2016-02-23 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
2015-12-28 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
2015-11-18 |
paulson |
New theorems mostly from Peter Gammie
|
file |
diff |
annotate
|
2015-11-11 |
Andreas Lochbihler |
add various lemmas
|
file |
diff |
annotate
|
2015-10-27 |
paulson |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
file |
diff |
annotate
|
2015-10-09 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
2015-09-21 |
paulson |
new lemmas and movement of lemmas into place
|
file |
diff |
annotate
|
2015-08-13 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
2015-05-26 |
paulson |
New material about paths, and some lemmas
|
file |
diff |
annotate
|
2015-02-11 |
Andreas Lochbihler |
add lemmas about bind and image
|
file |
diff |
annotate
|
2015-02-11 |
paulson |
Merge
|
file |
diff |
annotate
|
2015-02-10 |
paulson |
New lemmas and a bit of tidying up.
|
file |
diff |
annotate
|
2015-02-10 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
2014-10-30 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
2014-09-06 |
haftmann |
added various facts
|
file |
diff |
annotate
|
2014-09-01 |
blanchet |
tuned structure inclusion
|
file |
diff |
annotate
|
2014-06-21 |
ballarin |
Two basic lemmas on bij_betw.
|
file |
diff |
annotate
|
2014-04-16 |
haftmann |
more simp rules for Fun.swap
|
file |
diff |
annotate
|
2014-03-15 |
haftmann |
more complete set of lemmas wrt. image and composition
|
file |
diff |
annotate
|
2014-03-13 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
2014-03-09 |
haftmann |
bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices
|
file |
diff |
annotate
|
2014-03-07 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
2014-02-14 |
blanchet |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors)
|
file |
diff |
annotate
|
2014-02-12 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
2014-01-20 |
blanchet |
tuning
|
file |
diff |
annotate
|
2014-01-16 |
blanchet |
moved lemmas from 'Fun_More_FP' to where they belong
|
file |
diff |
annotate
|
2013-11-25 |
traytel |
eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
|
file |
diff |
annotate
|
2013-10-18 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
2013-09-26 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
2013-06-23 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
2013-04-18 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
2013-04-03 |
haftmann |
generalized lemma fold_image thanks to Peter Lammich
|
file |
diff |
annotate
|
2012-10-18 |
haftmann |
simp results for simplification results of Inf/Sup expressions on bool;
|
file |
diff |
annotate
|
2012-10-08 |
haftmann |
consolidated names of theorems on composition;
|
file |
diff |
annotate
|
2012-08-22 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
2012-04-19 |
huffman |
tuned lemmas (v)image_id;
|
file |
diff |
annotate
|
2012-04-15 |
haftmann |
centralized enriched_type declaration, thanks to in-situ available Isar commands
|
file |
diff |
annotate
|
2012-03-15 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
2012-02-22 |
bulwahn |
generalizing inj_on_Int
|
file |
diff |
annotate
|
2012-02-05 |
bulwahn |
removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)
|
file |
diff |
annotate
|
2012-02-05 |
bulwahn |
adding a remark about lemma which is too special and should be removed
|
file |
diff |
annotate
|
2011-11-20 |
wenzelm |
explicit is better than implicit;
|
file |
diff |
annotate
|
2011-10-19 |
bulwahn |
removing old code generator setup for function types
|
file |
diff |
annotate
|
2011-09-14 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|