| 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
|
| Wed, 30 Mar 2011 11:32:52 +0200 |
bulwahn |
renewing specifications in HOL: replacing types by type_synonym
|
file |
diff |
annotate
|
| Fri, 10 Dec 2010 16:10:50 +0100 |
haftmann |
moved most fundamental lemmas upwards
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 15:05:46 +0100 |
haftmann |
bot comes before top, inf before sup etc.
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:34:51 +0100 |
haftmann |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`;
|
file |
diff |
annotate
|
| Thu, 02 Dec 2010 14:34:58 +0100 |
hoelzl |
Move SUP_commute, SUP_less_iff to HOL image;
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 14:14:17 +0100 |
hoelzl |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
file |
diff |
annotate
|
| Fri, 01 Oct 2010 16:05:25 +0200 |
haftmann |
constant `contents` renamed to `the_elem`
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 10:45:55 +0200 |
nipkow |
put expand_(fun/set)_eq back in as synonyms, for compatibility
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 12:13:58 +0200 |
blanchet |
"no_atp" fact that leads to unsound proofs
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:56:30 +0200 |
blanchet |
"no_atp" a few facts that often lead to unsound proofs
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 16:54:42 +0200 |
haftmann |
qualified constants Set.member and Set.Collect
|
file |
diff |
annotate
|
| Tue, 08 Jun 2010 16:37:19 +0200 |
haftmann |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 12:50:38 -0700 |
huffman |
use lattice theorems to prove set theorems
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 15:44:06 +0100 |
hoelzl |
Added vimage_inter_cong
|
file |
diff |
annotate
|
| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Thu, 04 Feb 2010 14:45:08 +0100 |
hoelzl |
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Wed, 30 Dec 2009 10:24:53 +0100 |
krauss |
killed a few warnings
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 16:26:23 +0100 |
berghofe |
Removed eq_to_mono2, added not_mono.
|
file |
diff |
annotate
|
| Mon, 09 Nov 2009 15:50:15 +0000 |
paulson |
New theory Probability/Borel.thy, and some associated lemmas
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 11:19:11 +0100 |
paulson |
merged
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:32:51 +0100 |
paulson |
Some new lemmas concerning sets
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:16:25 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 21 Oct 2009 08:14:38 +0200 |
haftmann |
dropped redundant gen_ prefix
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 16:13:01 +0200 |
haftmann |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
file |
diff |
annotate
|
| Tue, 20 Oct 2009 15:02:48 +0100 |
paulson |
Removal of the unused atpset concept, the atp attribute and some related code.
|
file |
diff |
annotate
|
| Wed, 07 Oct 2009 14:01:26 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 19 Sep 2009 07:38:03 +0200 |
haftmann |
inter and union are mere abbreviations for inf and sup
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 14:09:42 +0200 |
nipkow |
tuned the simp rules for Int involving insert and intervals.
|
file |
diff |
annotate
|
| Tue, 28 Jul 2009 13:37:09 +0200 |
haftmann |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
file |
diff |
annotate
|
| Wed, 22 Jul 2009 18:02:10 +0200 |
haftmann |
moved complete_lattice &c. into separate theory
|
file |
diff |
annotate
|
| Wed, 22 Jul 2009 14:20:32 +0200 |
haftmann |
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 14:38:07 +0200 |
haftmann |
attempt for more concise setup of non-etacontracting binders
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 11:09:50 +0200 |
haftmann |
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 07:54:44 +0200 |
haftmann |
swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 15:24:15 +0200 |
haftmann |
less digestible
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 11:47:17 +0200 |
haftmann |
refined outline structure
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 09:52:09 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 08:31:12 +0200 |
haftmann |
closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 08:32:07 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 15:54:19 +0200 |
haftmann |
refinement of lattice classes
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 23:48:21 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 11 Jul 2009 21:33:01 +0200 |
haftmann |
added boolean_algebra type class; tuned lattice duals
|
file |
diff |
annotate
|
| Mon, 06 Jul 2009 21:24:30 +0200 |
wenzelm |
structure Thm: less pervasive names;
|
file |
diff |
annotate
|
| Mon, 15 Jun 2009 16:13:19 +0200 |
haftmann |
authentic syntax for Pow and image
|
file |
diff |
annotate
|
| Fri, 05 Jun 2009 08:06:03 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 15:28:59 +0200 |
haftmann |
insert now qualified and with authentic syntax
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 19:44:06 +0200 |
nipkow |
finite lemmas
|
file |
diff |
annotate
|
| Mon, 18 May 2009 23:15:38 +0200 |
nipkow |
fine-tuned elimination of comprehensions involving x=t.
|
file |
diff |
annotate
|
| Sat, 16 May 2009 11:28:02 +0200 |
nipkow |
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
|
file |
diff |
annotate
|
| Tue, 31 Mar 2009 13:23:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 14:08:41 +0100 |
haftmann |
tuned some theorem and attribute bindings
|
file |
diff |
annotate
|
| Sat, 14 Mar 2009 12:50:29 +0100 |
haftmann |
reverted to old version of Set.thy -- strange effects have to be traced first
|
file |
diff |
annotate
|
| Sat, 07 Mar 2009 15:20:32 +0100 |
haftmann |
restructured theory Set.thy
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:11 +0100 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 23:55:04 +0100 |
nipkow |
finiteness lemmas
|
file |
diff |
annotate
|
| Thu, 29 Jan 2009 22:28:03 +0100 |
berghofe |
Added strong congruence rule for UN.
|
file |
diff |
annotate
|
| Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
| Mon, 11 Aug 2008 14:50:00 +0200 |
haftmann |
rudimentary code setup for set operations
|
file |
diff |
annotate
|
| Tue, 01 Jul 2008 06:51:59 +0200 |
huffman |
remove simp attribute from range_composition
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:43 +0200 |
berghofe |
- Now uses Orderings as parent theory
|
file |
diff |
annotate
|
| Tue, 22 Apr 2008 08:33:16 +0200 |
haftmann |
constant HOL.eq now qualified
|
file |
diff |
annotate
|
| Wed, 02 Apr 2008 15:58:32 +0200 |
haftmann |
explicit class "eq" for operational equality
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:00 +0100 |
wenzelm |
replaced 'ML_setup' by 'ML';
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:47:35 +0100 |
wenzelm |
eliminated change_claset/simpset;
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:15 +0100 |
haftmann |
moved some set lemmas from Set.thy here
|
file |
diff |
annotate
|
| Fri, 25 Jan 2008 14:54:41 +0100 |
haftmann |
improved code theorem setup
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:02 +0100 |
haftmann |
splitted class uminus from class minus
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 20:13:03 +0100 |
haftmann |
adjustions to due to instance target
|
file |
diff |
annotate
|