| 2012-03-12 |
noschinl |
2012-03-12 |
tuned simpset
|
file | diff | annotate |
| 2012-03-09 |
haftmann |
2012-03-09 |
beautified
|
file | diff | annotate |
| 2012-02-16 |
bulwahn |
2012-02-16 |
removing unnecessary premise from diff_single_insert
|
file | diff | annotate |
| 2012-02-14 |
wenzelm |
2012-02-14 |
eliminated obsolete aliases;
|
file | diff | annotate |
| 2012-01-07 |
haftmann |
2012-01-07 |
massaging of code setup for sets
|
file | diff | annotate |
| 2012-01-06 |
haftmann |
2012-01-06 |
incorporated various theorems from theory More_Set into corpus
|
file | diff | annotate |
| 2012-01-06 |
wenzelm |
2012-01-06 |
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 |
2012-01-01 |
interaction of set operations for execution and membership predicate
|
file | diff | annotate |
| 2012-01-01 |
haftmann |
2012-01-01 |
cleanup of code declarations
|
file | diff | annotate |
| 2011-12-29 |
haftmann |
2011-12-29 |
fundamental theorems on Set.bind
|
file | diff | annotate |
| 2011-12-29 |
haftmann |
2011-12-29 |
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 |
2011-12-26 |
moved various set operations to theory Set (resp. Product_Type)
|
file | diff | annotate |
| 2011-12-24 |
haftmann |
2011-12-24 |
`set` is now a proper type constructor; added operation for set monad
|
file | diff | annotate |
| 2011-12-17 |
wenzelm |
2011-12-17 |
tuned signature;
|
file | diff | annotate |
| 2011-11-27 |
wenzelm |
2011-11-27 |
just one data slot per module;
tuned;
|
file | diff | annotate |
| 2011-11-24 |
wenzelm |
2011-11-24 |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file | diff | annotate |
| 2011-11-20 |
wenzelm |
2011-11-20 |
eliminated obsolete "standard";
|
file | diff | annotate |
| 2011-10-16 |
haftmann |
2011-10-16 |
hide not_member as also member
|
file | diff | annotate |
| 2011-10-09 |
huffman |
2011-10-09 |
Set.thy: remove redundant [simp] declarations
|
file | diff | annotate |
| 2011-09-06 |
nipkow |
2011-09-06 |
added new lemmas
|
file | diff | annotate |
| 2011-08-25 |
krauss |
2011-08-25 |
lemma Compl_insert: "- insert x A = (-A) - {x}"
|
file | diff | annotate |
| 2011-08-17 |
wenzelm |
2011-08-17 |
modernized signature of Term.absfree/absdummy;
eliminated obsolete Term.list_abs_free;
|
file | diff | annotate |
| 2011-07-24 |
haftmann |
2011-07-24 |
more coherent structure in and across theories
|
file | diff | annotate |
| 2011-07-18 |
haftmann |
2011-07-18 |
moved lemmas to appropriate theory
|
file | diff | annotate |
| 2011-07-17 |
haftmann |
2011-07-17 |
moving UNIV = ... equations to their proper theories
|
file | diff | annotate |
| 2011-07-14 |
haftmann |
2011-07-14 |
tuned lemma positions and proofs
|
file | diff | annotate |
| 2011-04-22 |
wenzelm |
2011-04-22 |
misc tuning and simplification;
|
file | diff | annotate |
| 2011-04-22 |
wenzelm |
2011-04-22 |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
tuned signature;
|
file | diff | annotate |
| 2011-04-22 |
wenzelm |
2011-04-22 |
modernized Quantifier1 simproc setup;
|
file | diff | annotate |
| 2011-04-08 |
wenzelm |
2011-04-08 |
discontinued special treatment of structure Mixfix;
eliminated slightly odd no_syn convenience;
|
file | diff | annotate |
| 2011-04-08 |
wenzelm |
2011-04-08 |
explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;
|
file | diff | annotate |
| 2011-03-30 |
bulwahn |
2011-03-30 |
renewing specifications in HOL: replacing types by type_synonym
|
file | diff | annotate |
| 2010-12-10 |
haftmann |
2010-12-10 |
moved most fundamental lemmas upwards
|
file | diff | annotate |
| 2010-12-08 |
haftmann |
2010-12-08 |
bot comes before top, inf before sup etc.
|
file | diff | annotate |
| 2010-12-08 |
haftmann |
2010-12-08 |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`;
tuned
|
file | diff | annotate |
| 2010-12-02 |
hoelzl |
2010-12-02 |
Move SUP_commute, SUP_less_iff to HOL image;
Cleanup generic complete_lattice lemmas in Positive_Infinite_Real;
Cleanup lemma positive_integral_alt;
|
file | diff | annotate |
| 2010-11-23 |
hoelzl |
2010-11-23 |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file | diff | annotate |
| 2010-10-01 |
haftmann |
2010-10-01 |
constant `contents` renamed to `the_elem`
|
file | diff | annotate |
| 2010-09-13 |
nipkow |
2010-09-13 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| 2010-09-08 |
nipkow |
2010-09-08 |
put expand_(fun/set)_eq back in as synonyms, for compatibility
|
file | diff | annotate |
| 2010-09-07 |
nipkow |
2010-09-07 |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
file | diff | annotate |
| 2010-08-28 |
haftmann |
2010-08-28 |
formerly unnamed infix equality now named HOL.eq
|
file | diff | annotate |
| 2010-08-27 |
haftmann |
2010-08-27 |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file | diff | annotate |
| 2010-08-26 |
haftmann |
2010-08-26 |
formerly unnamed infix impliciation now named HOL.implies
|
file | diff | annotate |
| 2010-08-25 |
wenzelm |
2010-08-25 |
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 |
2010-08-23 |
"no_atp" fact that leads to unsound proofs
|
file | diff | annotate |
| 2010-08-23 |
blanchet |
2010-08-23 |
"no_atp" a few facts that often lead to unsound proofs
|
file | diff | annotate |
| 2010-07-12 |
haftmann |
2010-07-12 |
dropped superfluous [code del]s
|
file | diff | annotate |
| 2010-07-01 |
haftmann |
2010-07-01 |
qualified constants Set.member and Set.Collect
|
file | diff | annotate |
| 2010-06-08 |
haftmann |
2010-06-08 |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
file | diff | annotate |
| 2010-03-28 |
huffman |
2010-03-28 |
use lattice theorems to prove set theorems
|
file | diff | annotate |
| 2010-03-18 |
blanchet |
2010-03-18 |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file | diff | annotate |
| 2010-03-04 |
hoelzl |
2010-03-04 |
Added vimage_inter_cong
|
file | diff | annotate |
| 2010-03-01 |
haftmann |
2010-03-01 |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file | diff | annotate |
| 2010-02-11 |
wenzelm |
2010-02-11 |
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
|
file | diff | annotate |
| 2010-02-04 |
hoelzl |
2010-02-04 |
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
|
file | diff | annotate |
| 2010-01-28 |
haftmann |
2010-01-28 |
new theory Algebras.thy for generic algebraic structures
|
file | diff | annotate |
| 2009-12-30 |
krauss |
2009-12-30 |
killed a few warnings
|
file | diff | annotate |
| 2009-11-27 |
berghofe |
2009-11-27 |
Removed eq_to_mono2, added not_mono.
|
file | diff | annotate |
| 2009-11-09 |
paulson |
2009-11-09 |
New theory Probability/Borel.thy, and some associated lemmas
|
file | diff | annotate |