| 2016-05-27 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| 2016-05-23 |
paulson |
Lots of new material for multivariate analysis
|
file |
diff |
annotate
|
| 2016-05-17 |
eberlm |
Moved material from AFP/Randomised_Social_Choice to distribution
|
file |
diff |
annotate
|
| 2016-05-09 |
paulson |
renamings and refinements
|
file |
diff |
annotate
|
| 2016-04-18 |
paulson |
new theorems about convex hulls, etc.; also, renamed some theorems
|
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-05 |
wenzelm |
old HOL syntax is for input only;
|
file |
diff |
annotate
|
| 2016-02-23 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| 2016-01-07 |
paulson |
revisions to limits and derivatives, plus new lemmas
|
file |
diff |
annotate
|
| 2016-01-06 |
hoelzl |
add the proof of the central limit theorem
|
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-10-26 |
paulson |
new lemmas about topology, etc., for Cauchy integral formula
|
file |
diff |
annotate
|
| 2015-10-09 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| 2015-10-02 |
paulson |
New theorems about connected sets. And pairwise moved to Set.thy.
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2015-05-01 |
nipkow |
new simp rule
|
file |
diff |
annotate
|
| 2015-04-14 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
| 2015-02-11 |
paulson |
Merge
|
file |
diff |
annotate
|
| 2015-02-10 |
paulson |
Not a simprule, as it complicates proofs
|
file |
diff |
annotate
|
| 2015-02-10 |
paulson |
New lemmas and a bit of tidying up.
|
file |
diff |
annotate
|
| 2015-02-10 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| 2015-02-10 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| 2014-11-13 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| 2014-11-10 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
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-04-26 |
haftmann |
tuned
|
file |
diff |
annotate
|
| 2014-03-13 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| 2014-03-09 |
haftmann |
tuned;
|
file |
diff |
annotate
|
| 2014-02-27 |
paulson |
A bit of tidying up
|
file |
diff |
annotate
|
| 2014-01-25 |
wenzelm |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
file |
diff |
annotate
|
| 2014-01-12 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2013-10-18 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| 2013-09-02 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| 2013-05-25 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| 2013-04-18 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| 2013-04-12 |
wenzelm |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
file |
diff |
annotate
|
| 2013-03-12 |
nipkow |
extended set comprehension notation with {pttrn : A . P}
|
file |
diff |
annotate
|
| 2013-03-05 |
nipkow |
more lemmas about intervals
|
file |
diff |
annotate
|
| 2013-02-17 |
haftmann |
Sieve of Eratosthenes
|
file |
diff |
annotate
|
| 2012-12-17 |
nipkow |
made element and subset relations non-associative (just like all orderings)
|
file |
diff |
annotate
|
| 2012-10-09 |
kuncar |
rename Set.project to Set.filter - more appropriate name
|
file |
diff |
annotate
|
| 2012-09-29 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
| 2012-04-06 |
haftmann |
tuned
|
file |
diff |
annotate
|
| 2012-03-12 |
noschinl |
tuned simpset
|
file |
diff |
annotate
|
| 2012-03-09 |
haftmann |
beautified
|
file |
diff |
annotate
|
| 2012-02-16 |
bulwahn |
removing unnecessary premise from diff_single_insert
|
file |
diff |
annotate
|
| 2012-02-14 |
wenzelm |
eliminated obsolete aliases;
|
file |
diff |
annotate
|
| 2012-01-07 |
haftmann |
massaging of code setup for sets
|
file |
diff |
annotate
|
| 2012-01-06 |
haftmann |
incorporated various theorems from theory More_Set into corpus
|
file |
diff |
annotate
|
| 2012-01-06 |
wenzelm |
tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);
|
file |
diff |
annotate
|
| 2012-01-01 |
haftmann |
interaction of set operations for execution and membership predicate
|
file |
diff |
annotate
|
| 2012-01-01 |
haftmann |
cleanup of code declarations
|
file |
diff |
annotate
|
| 2011-12-29 |
haftmann |
fundamental theorems on Set.bind
|
file |
diff |
annotate
|
| 2011-12-29 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
|
file |
diff |
annotate
|
| 2011-12-26 |
haftmann |
moved various set operations to theory Set (resp. Product_Type)
|
file |
diff |
annotate
|
| 2011-12-24 |
haftmann |
`set` is now a proper type constructor; added operation for set monad
|
file |
diff |
annotate
|
| 2011-12-17 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 2011-11-27 |
wenzelm |
just one data slot per module;
|
file |
diff |
annotate
|
| 2011-11-24 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| 2011-11-20 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| 2011-10-16 |
haftmann |
hide not_member as also member
|
file |
diff |
annotate
|
| 2011-10-09 |
huffman |
Set.thy: remove redundant [simp] declarations
|
file |
diff |
annotate
|
| 2011-09-06 |
nipkow |
added new lemmas
|
file |
diff |
annotate
|
| 2011-08-25 |
krauss |
lemma Compl_insert: "- insert x A = (-A) - {x}"
|
file |
diff |
annotate
|
| 2011-08-17 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| 2011-07-24 |
haftmann |
more coherent structure in and across theories
|
file |
diff |
annotate
|
| 2011-07-18 |
haftmann |
moved lemmas to appropriate theory
|
file |
diff |
annotate
|
| 2011-07-17 |
haftmann |
moving UNIV = ... equations to their proper theories
|
file |
diff |
annotate
|
| 2011-07-13 |
haftmann |
tuned lemma positions and proofs
|
file |
diff |
annotate
|
| 2011-04-22 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| 2011-04-22 |
wenzelm |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
|
file |
diff |
annotate
|
| 2011-04-22 |
wenzelm |
modernized Quantifier1 simproc setup;
|
file |
diff |
annotate
|
| 2011-04-08 |
wenzelm |
discontinued special treatment of structure Mixfix;
|
file |
diff |
annotate
|
| 2011-04-08 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| 2011-03-30 |
bulwahn |
renewing specifications in HOL: replacing types by type_synonym
|
file |
diff |
annotate
|
| 2010-12-10 |
haftmann |
moved most fundamental lemmas upwards
|
file |
diff |
annotate
|
| 2010-12-08 |
haftmann |
bot comes before top, inf before sup etc.
|
file |
diff |
annotate
|
| 2010-12-08 |
haftmann |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`;
|
file |
diff |
annotate
|
| 2010-12-02 |
hoelzl |
Move SUP_commute, SUP_less_iff to HOL image;
|
file |
diff |
annotate
|
| 2010-11-23 |
hoelzl |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file |
diff |
annotate
|
| 2010-10-01 |
haftmann |
constant `contents` renamed to `the_elem`
|
file |
diff |
annotate
|
| 2010-09-13 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| 2010-09-08 |
nipkow |
put expand_(fun/set)_eq back in as synonyms, for compatibility
|
file |
diff |
annotate
|
| 2010-09-07 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| 2010-08-28 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| 2010-08-27 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| 2010-08-26 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| 2010-08-25 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| 2010-08-23 |
blanchet |
"no_atp" fact that leads to unsound proofs
|
file |
diff |
annotate
|
| 2010-08-23 |
blanchet |
"no_atp" a few facts that often lead to unsound proofs
|
file |
diff |
annotate
|
| 2010-07-12 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| 2010-07-01 |
haftmann |
qualified constants Set.member and Set.Collect
|
file |
diff |
annotate
|
| 2010-06-08 |
haftmann |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
file |
diff |
annotate
|
| 2010-03-28 |
huffman |
use lattice theorems to prove set theorems
|
file |
diff |
annotate
|
| 2010-03-18 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| 2010-03-04 |
hoelzl |
Added vimage_inter_cong
|
file |
diff |
annotate
|
| 2010-03-01 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| 2010-02-11 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| 2010-02-04 |
hoelzl |
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
|
file |
diff |
annotate
|
| 2010-01-28 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| 2009-12-30 |
krauss |
killed a few warnings
|
file |
diff |
annotate
|
| 2009-11-27 |
berghofe |
Removed eq_to_mono2, added not_mono.
|
file |
diff |
annotate
|
| 2009-11-09 |
paulson |
New theory Probability/Borel.thy, and some associated lemmas
|
file |
diff |
annotate
|
| 2009-10-21 |
paulson |
merged
|
file |
diff |
annotate
|
| 2009-10-20 |
paulson |
Some new lemmas concerning sets
|
file |
diff |
annotate
|
| 2009-10-21 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-10-21 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| 2009-10-20 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| 2009-10-20 |
paulson |
Removal of the unused atpset concept, the atp attribute and some related code.
|
file |
diff |
annotate
|
| 2009-10-07 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| 2009-09-19 |
haftmann |
inter and union are mere abbreviations for inf and sup
|
file |
diff |
annotate
|
| 2009-08-31 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
file |
diff |
annotate
|
| 2009-07-28 |
haftmann |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
file |
diff |
annotate
|
| 2009-07-22 |
haftmann |
moved complete_lattice &c. into separate theory
|
file |
diff |
annotate
|
| 2009-07-22 |
haftmann |
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
|
file |
diff |
annotate
|
| 2009-07-21 |
haftmann |
attempt for more concise setup of non-etacontracting binders
|
file |
diff |
annotate
|
| 2009-07-21 |
haftmann |
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
|
file |
diff |
annotate
|
| 2009-07-21 |
haftmann |
swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
|
file |
diff |
annotate
|