| Fri, 01 May 2015 08:45:30 +0200 |
nipkow |
new simp rule
|
file |
diff |
annotate
|
| Tue, 14 Apr 2015 11:32:01 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 12:01:56 +0000 |
paulson |
Merge
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 17:37:06 +0000 |
paulson |
Not a simprule, as it complicates proofs
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 16:08:11 +0000 |
paulson |
New lemmas and a bit of tidying up.
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 16:46:21 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:25:45 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 08:56:08 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 22:45:07 +0100 |
haftmann |
tuned;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 16:07:21 +0000 |
paulson |
A bit of tidying up
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 22:06:07 +0100 |
wenzelm |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
file |
diff |
annotate
|
| Sun, 12 Jan 2014 14:32:22 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Mon, 02 Sep 2013 17:12:59 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Fri, 12 Apr 2013 17:21:51 +0200 |
wenzelm |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
file |
diff |
annotate
|
| Tue, 12 Mar 2013 07:51:10 +0100 |
nipkow |
extended set comprehension notation with {pttrn : A . P}
|
file |
diff |
annotate
|
| Tue, 05 Mar 2013 10:16:15 +0100 |
nipkow |
more lemmas about intervals
|
file |
diff |
annotate
|
| Sun, 17 Feb 2013 21:29:30 +0100 |
haftmann |
Sieve of Eratosthenes
|
file |
diff |
annotate
|
| Mon, 17 Dec 2012 17:19:21 +0100 |
nipkow |
made element and subset relations non-associative (just like all orderings)
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 16:57:58 +0200 |
kuncar |
rename Set.project to Set.filter - more appropriate name
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 18:23:46 +0200 |
wenzelm |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 19:18:00 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 15:11:24 +0100 |
noschinl |
tuned simpset
|
file |
diff |
annotate
|
| Fri, 09 Mar 2012 21:50:27 +0100 |
haftmann |
beautified
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 16:02:02 +0100 |
bulwahn |
removing unnecessary premise from diff_single_insert
|
file |
diff |
annotate
|
| Tue, 14 Feb 2012 17:11:33 +0100 |
wenzelm |
eliminated obsolete aliases;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2012 20:44:23 +0100 |
haftmann |
massaging of code setup for sets
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 21:48:45 +0100 |
haftmann |
incorporated various theorems from theory More_Set into corpus
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 16:45:19 +0100 |
wenzelm |
tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);
|
file |
diff |
annotate
|
| Sun, 01 Jan 2012 15:44:15 +0100 |
haftmann |
interaction of set operations for execution and membership predicate
|
file |
diff |
annotate
|
| Sun, 01 Jan 2012 11:28:45 +0100 |
haftmann |
cleanup of code declarations
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 14:23:40 +0100 |
haftmann |
fundamental theorems on Set.bind
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:54 +0100 |
haftmann |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat
|
file |
diff |
annotate
|
| Mon, 26 Dec 2011 18:32:43 +0100 |
haftmann |
moved various set operations to theory Set (resp. Product_Type)
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:07 +0100 |
haftmann |
`set` is now a proper type constructor; added operation for set monad
|
file |
diff |
annotate
|
| Sat, 17 Dec 2011 13:08:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 22:03:22 +0100 |
wenzelm |
just one data slot per module;
|
file |
diff |
annotate
|
| Thu, 24 Nov 2011 21:01:06 +0100 |
wenzelm |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Sun, 16 Oct 2011 14:48:00 +0200 |
haftmann |
hide not_member as also member
|
file |
diff |
annotate
|
| Sun, 09 Oct 2011 08:30:48 +0200 |
huffman |
Set.thy: remove redundant [simp] declarations
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 14:25:16 +0200 |
nipkow |
added new lemmas
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 14:06:34 +0200 |
krauss |
lemma Compl_insert: "- insert x A = (-A) - {x}"
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
| Sun, 24 Jul 2011 21:27:25 +0200 |
haftmann |
more coherent structure in and across theories
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 21:15:51 +0200 |
haftmann |
moved lemmas to appropriate theory
|
file |
diff |
annotate
|
| Sun, 17 Jul 2011 19:48:02 +0200 |
haftmann |
moving UNIV = ... equations to their proper theories
|
file |
diff |
annotate
|
| Thu, 14 Jul 2011 00:20:43 +0200 |
haftmann |
tuned lemma positions and proofs
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 15:05:04 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 14:30:32 +0200 |
wenzelm |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61);
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 13:58:13 +0200 |
wenzelm |
modernized Quantifier1 simproc setup;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 14:20:57 +0200 |
wenzelm |
discontinued special treatment of structure Mixfix;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|