| 2015-05-01 |
nipkow |
2015-05-01 |
new simp rule
|
file | diff | annotate |
| 2015-04-14 |
Andreas Lochbihler |
2015-04-14 |
add lemmas
|
file | diff | annotate |
| 2015-02-11 |
paulson |
2015-02-11 |
Merge
|
file | diff | annotate |
| 2015-02-10 |
paulson |
2015-02-10 |
Not a simprule, as it complicates proofs
|
file | diff | annotate |
| 2015-02-10 |
paulson |
2015-02-10 |
New lemmas and a bit of tidying up.
|
file | diff | annotate |
| 2015-02-10 |
wenzelm |
2015-02-10 |
misc tuning;
|
file | diff | annotate |
| 2015-02-10 |
wenzelm |
2015-02-10 |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
|
file | diff | annotate |
| 2014-11-13 |
hoelzl |
2014-11-13 |
import general theorems from AFP/Markov_Models
|
file | diff | annotate |
| 2014-11-10 |
wenzelm |
2014-11-10 |
proper context for assume_tac (atac remains as fall-back without context);
|
file | diff | annotate |
| 2014-11-02 |
wenzelm |
2014-11-02 |
modernized header uniformly as section;
|
file | diff | annotate |
| 2014-10-30 |
wenzelm |
2014-10-30 |
eliminated aliases;
|
file | diff | annotate |
| 2014-04-26 |
haftmann |
2014-04-26 |
tuned
|
file | diff | annotate |
| 2014-03-13 |
haftmann |
2014-03-13 |
tuned proofs
|
file | diff | annotate |
| 2014-03-09 |
haftmann |
2014-03-09 |
tuned;
elimination rule subset_imageE;
typical composition collapsing rewrite order in lemma image_image_eq_image_comp;
destruction rules ball_imageD, bex_imageD
|
file | diff | annotate |
| 2014-02-27 |
paulson |
2014-02-27 |
A bit of tidying up
|
file | diff | annotate |
| 2014-01-25 |
wenzelm |
2014-01-25 |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
file | diff | annotate |
| 2014-01-12 |
wenzelm |
2014-01-12 |
tuned signature;
clarified context;
|
file | diff | annotate |
| 2013-10-18 |
blanchet |
2013-10-18 |
killed most "no_atp", to make Sledgehammer more complete
|
file | diff | annotate |
| 2013-09-02 |
nipkow |
2013-09-02 |
added lemmas
|
file | diff | annotate |
| 2013-05-25 |
wenzelm |
2013-05-25 |
syntax translations always depend on context;
|
file | diff | annotate |
| 2013-04-18 |
wenzelm |
2013-04-18 |
simplifier uses proper Proof.context instead of historic type simpset;
|
file | diff | annotate |
| 2013-04-12 |
wenzelm |
2013-04-12 |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
file | diff | annotate |
| 2013-03-12 |
nipkow |
2013-03-12 |
extended set comprehension notation with {pttrn : A . P}
|
file | diff | annotate |
| 2013-03-05 |
nipkow |
2013-03-05 |
more lemmas about intervals
|
file | diff | annotate |
| 2013-02-17 |
haftmann |
2013-02-17 |
Sieve of Eratosthenes
|
file | diff | annotate |
| 2012-12-17 |
nipkow |
2012-12-17 |
made element and subset relations non-associative (just like all orderings)
|
file | diff | annotate |
| 2012-10-09 |
kuncar |
2012-10-09 |
rename Set.project to Set.filter - more appropriate name
|
file | diff | annotate |
| 2012-09-29 |
wenzelm |
2012-09-29 |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file | diff | annotate |
| 2012-04-06 |
haftmann |
2012-04-06 |
tuned
|
file | diff | annotate |
| 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 |