#
6e43b5b0 |
|
27-Aug-2019 |
nipkow <none@none> |
moved lemmas
|
#
945c5111 |
|
26-Mar-2019 |
paulson <lp15@cam.ac.uk> |
generalised homotopic_with to topologies; homotopic_with_canon is the old version
|
#
b0924e81 |
|
21-Mar-2019 |
paulson <lp15@cam.ac.uk> |
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
|
#
e977f1fa |
|
31-Jan-2019 |
haftmann <none@none> |
proper congruence rule for image operator --HG-- extra : rebase_source : 71f59936260619419f4d3f7f86d1b930bc771065
|
#
ab32308e |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
renamings and new material
|
#
083015db |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
new material about summations and powers, along with some tweaks
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
ec600d16 |
|
30-Dec-2018 |
haftmann <none@none> |
prefer naming convention from datatype package for strong congruence rules
|
#
527bcc61 |
|
11-Nov-2018 |
nipkow <none@none> |
more [simp]
|
#
1e9e4316 |
|
31-Oct-2018 |
wenzelm <none@none> |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
#
6fd6219b |
|
21-Oct-2018 |
nipkow <none@none> |
uniform naming of strong congruence rules
|
#
b1eea222 |
|
21-Oct-2018 |
nipkow <none@none> |
added lemma
|
#
5abaa1a1 |
|
17-Oct-2018 |
paulson <lp15@cam.ac.uk> |
new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
|
#
95b20e9c |
|
21-Aug-2018 |
haftmann <none@none> |
new simp rule --HG-- extra : rebase_source : 7b4d8565548968b9b9b00ef5d005f85ec45706d2
|
#
d463f754 |
|
19-Feb-2018 |
paulson <lp15@cam.ac.uk> |
lots of new material, ultimately related to measure theory
|
#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
#
91335636 |
|
11-Jan-2018 |
nipkow <none@none> |
line break before op was intentional
|
#
019f7b3e |
|
10-Jan-2018 |
nipkow <none@none> |
tuned notation
|
#
20349da0 |
|
10-Jan-2018 |
nipkow <none@none> |
Manual updates towards conversion of "op" syntax --HG-- extra : amend_source : fd689f9cef643a634d5ce2dfded9a17206473899
|
#
fea44565 |
|
31-Dec-2017 |
paulson <lp15@cam.ac.uk> |
Restored correct spacing for set comprehensions
|
#
fea6a4cc |
|
22-Dec-2017 |
paulson <lp15@cam.ac.uk> |
new/improved theories involving convergence; better pretty-printing for bounded quantifiers and sum/product
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
85b3e948 |
|
11-Nov-2017 |
haftmann <none@none> |
dedicated definition for coprimality --HG-- extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae
|
#
476ac5bb |
|
08-Oct-2017 |
haftmann <none@none> |
canonical introduction and destruction rules for pairwise --HG-- extra : rebase_source : 4b2f35fa103369ed3a81ec56ba05c3a18d42b5e4
|
#
9ce4b661 |
|
29-Sep-2016 |
hoelzl <none@none> |
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
|
#
dc1c0020 |
|
28-Sep-2016 |
paulson <lp15@cam.ac.uk> |
new material connected with HOL Light measure theory, plus more rationalisation
|
#
14b782c6 |
|
22-Sep-2016 |
paulson <lp15@cam.ac.uk> |
More mainly topological results
|
#
1e83a38a |
|
15-Sep-2016 |
paulson <lp15@cam.ac.uk> |
simple new lemmas, mostly about sets
|
#
f937778a |
|
02-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
b78a0c93 |
|
05-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
aa4a4f88 |
|
05-Jul-2016 |
wenzelm <none@none> |
tuned;
|
#
0f0a91d1 |
|
02-Jul-2016 |
haftmann <none@none> |
more theorems
|
#
ff1efdae |
|
19-Jun-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
df3a0d7b |
|
14-Jun-2016 |
paulson <lp15@cam.ac.uk> |
new results about topology
|
#
9ebcfa62 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs;
|
#
b5509112 |
|
23-May-2016 |
paulson <lp15@cam.ac.uk> |
Lots of new material for multivariate analysis
|
#
94ba250a |
|
17-May-2016 |
eberlm <none@none> |
Moved material from AFP/Randomised_Social_Choice to distribution
|
#
6396ec02 |
|
09-May-2016 |
paulson <lp15@cam.ac.uk> |
renamings and refinements
|
#
e4b45827 |
|
18-Apr-2016 |
paulson <lp15@cam.ac.uk> |
new theorems about convex hulls, etc.; also, renamed some theorems
|
#
0700f7dc |
|
04-Apr-2016 |
paulson <lp15@cam.ac.uk> |
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
|
#
7a677ca9 |
|
05-Mar-2016 |
wenzelm <none@none> |
old HOL syntax is for input only;
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
8b08bf14 |
|
07-Jan-2016 |
paulson <none@none> |
revisions to limits and derivatives, plus new lemmas
|
#
5ad25152 |
|
05-Jan-2016 |
hoelzl <none@none> |
add the proof of the central limit theorem --HG-- extra : rebase_source : 493d99e28392771c51f4102a11b90533880e289f extra : amend_source : 3fb7b7c607104e57a2c3ba7f733dd570eb42fa3b
|
#
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
b7a36669 |
|
26-Oct-2015 |
paulson <none@none> |
new lemmas about topology, etc., for Cauchy integral formula
|
#
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
#
810d7742 |
|
02-Oct-2015 |
paulson <lp15@cam.ac.uk> |
New theorems about connected sets. And pairwise moved to Set.thy.
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
d9fa5894 |
|
01-May-2015 |
nipkow <none@none> |
new simp rule
|
#
b4ae9938 |
|
14-Apr-2015 |
Andreas Lochbihler <none@none> |
add lemmas
|
#
8f7c4718 |
|
10-Feb-2015 |
paulson <lp15@cam.ac.uk> |
Not a simprule, as it complicates proofs
|
#
7145f505 |
|
10-Feb-2015 |
paulson <lp15@cam.ac.uk> |
New lemmas and a bit of tidying up.
|
#
a9c547a6 |
|
10-Feb-2015 |
wenzelm <none@none> |
misc tuning;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
#
4eae0352 |
|
10-Nov-2014 |
wenzelm <none@none> |
proper context for assume_tac (atac remains as fall-back without context);
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
233ef912 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
55b2e577 |
|
26-Apr-2014 |
haftmann <none@none> |
tuned --HG-- extra : rebase_source : ec19f13e8067586494f4cc6530970036992e80cd
|
#
462f1580 |
|
13-Mar-2014 |
haftmann <none@none> |
tuned proofs
|
#
f3e9db36 |
|
09-Mar-2014 |
haftmann <none@none> |
tuned; elimination rule subset_imageE; typical composition collapsing rewrite order in lemma image_image_eq_image_comp; destruction rules ball_imageD, bex_imageD
|
#
26bd6171 |
|
27-Feb-2014 |
paulson <lp15@cam.ac.uk> |
A bit of tidying up
|
#
b96e01d8 |
|
25-Jan-2014 |
wenzelm <none@none> |
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
|
#
8aa502e5 |
|
12-Jan-2014 |
wenzelm <none@none> |
tuned signature; clarified context;
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
f21626ba |
|
02-Sep-2013 |
nipkow <none@none> |
added lemmas
|
#
ffcd6989 |
|
25-May-2013 |
wenzelm <none@none> |
syntax translations always depend on context;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
d8ea875e |
|
12-Apr-2013 |
wenzelm <none@none> |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
#
fa669f17 |
|
12-Mar-2013 |
nipkow <none@none> |
extended set comprehension notation with {pttrn : A . P}
|
#
3f8c7efb |
|
05-Mar-2013 |
nipkow <none@none> |
more lemmas about intervals
|
#
6b8e5a08 |
|
17-Feb-2013 |
haftmann <none@none> |
Sieve of Eratosthenes
|
#
b3668b1f |
|
17-Dec-2012 |
nipkow <none@none> |
made element and subset relations non-associative (just like all orderings)
|
#
8f15c228 |
|
09-Oct-2012 |
kuncar <none@none> |
rename Set.project to Set.filter - more appropriate name
|
#
4f9330a5 |
|
29-Sep-2012 |
wenzelm <none@none> |
more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
|
#
864691f8 |
|
06-Apr-2012 |
haftmann <none@none> |
tuned
|
#
f9af5d85 |
|
12-Mar-2012 |
noschinl <none@none> |
tuned simpset
|
#
74604767 |
|
09-Mar-2012 |
haftmann <none@none> |
beautified
|
#
4a9b615b |
|
16-Feb-2012 |
bulwahn <none@none> |
removing unnecessary premise from diff_single_insert
|
#
d1c16d1c |
|
14-Feb-2012 |
wenzelm <none@none> |
eliminated obsolete aliases;
|
#
12f40542 |
|
07-Jan-2012 |
haftmann <none@none> |
massaging of code setup for sets --HG-- extra : rebase_source : d88e8eabd9d4067b161ff0d4e077408f826712f8
|
#
55804831 |
|
06-Jan-2012 |
haftmann <none@none> |
incorporated various theorems from theory More_Set into corpus --HG-- extra : rebase_source : 3382b66ad31349cb7368f064c467aa4a53845dd2
|
#
e56fa193 |
|
06-Jan-2012 |
wenzelm <none@none> |
tuned -- more direct @{type_name set} (NB: binder_tr' retains the original non-syntax type for the bound/free variable);
|
#
4cd57042 |
|
01-Jan-2012 |
haftmann <none@none> |
interaction of set operations for execution and membership predicate --HG-- extra : rebase_source : 88e19fdc682e81ad835b4c75d2758a6cba48e84a
|
#
26ada052 |
|
01-Jan-2012 |
haftmann <none@none> |
cleanup of code declarations --HG-- extra : rebase_source : 7376929a640011e27309be6654ccf370df37e60a
|
#
0c69faee |
|
29-Dec-2011 |
haftmann <none@none> |
fundamental theorems on Set.bind --HG-- extra : rebase_source : f60f78a12efe9f4496619a04d48afb38f7eccb9d
|
#
ba37de4c |
|
29-Dec-2011 |
haftmann <none@none> |
semiring_numeral_0_eq_0, semiring_numeral_1_eq_1 now [simp], superseeding corresponding simp rules on type nat --HG-- extra : rebase_source : 7ed52e71daa69142f147737027b94acaef451223
|
#
f15c080b |
|
26-Dec-2011 |
haftmann <none@none> |
moved various set operations to theory Set (resp. Product_Type)
|
#
217d74c2 |
|
24-Dec-2011 |
haftmann <none@none> |
`set` is now a proper type constructor; added operation for set monad
|
#
4dbfb147 |
|
17-Dec-2011 |
wenzelm <none@none> |
tuned signature;
|
#
0bfc5cd8 |
|
27-Nov-2011 |
wenzelm <none@none> |
just one data slot per module; tuned;
|
#
1d553e50 |
|
24-Nov-2011 |
wenzelm <none@none> |
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
|
#
a495a026 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
#
37218fad |
|
16-Oct-2011 |
haftmann <none@none> |
hide not_member as also member
|
#
d372912f |
|
09-Oct-2011 |
huffman <none@none> |
Set.thy: remove redundant [simp] declarations
|
#
4c98af0b |
|
06-Sep-2011 |
nipkow <none@none> |
added new lemmas
|
#
12c07d40 |
|
25-Aug-2011 |
krauss <none@none> |
lemma Compl_insert: "- insert x A = (-A) - {x}"
|
#
7b43a234 |
|
17-Aug-2011 |
wenzelm <none@none> |
modernized signature of Term.absfree/absdummy; eliminated obsolete Term.list_abs_free;
|
#
6d1f4b94 |
|
24-Jul-2011 |
haftmann <none@none> |
more coherent structure in and across theories
|
#
3eec6301 |
|
18-Jul-2011 |
haftmann <none@none> |
moved lemmas to appropriate theory
|
#
eb0f3940 |
|
17-Jul-2011 |
haftmann <none@none> |
moving UNIV = ... equations to their proper theories
|
#
41c2c773 |
|
13-Jul-2011 |
haftmann <none@none> |
tuned lemma positions and proofs
|
#
c6e0bbb6 |
|
22-Apr-2011 |
wenzelm <none@none> |
misc tuning and simplification;
|
#
b95224b1 |
|
22-Apr-2011 |
wenzelm <none@none> |
proper context for Quantifier1 simprocs (avoid bad ProofContext.init_global from abc655166d61); tuned signature;
|
#
f1968c93 |
|
22-Apr-2011 |
wenzelm <none@none> |
modernized Quantifier1 simproc setup;
|
#
a4d04f8b |
|
08-Apr-2011 |
wenzelm <none@none> |
discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;
|
#
1c017ad4 |
|
08-Apr-2011 |
wenzelm <none@none> |
explicit structure Syntax_Trans; discontinued old-style constrainAbsC; --HG-- rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML
|
#
0d0a8a60 |
|
30-Mar-2011 |
bulwahn <none@none> |
renewing specifications in HOL: replacing types by type_synonym
|
#
100b174d |
|
10-Dec-2010 |
haftmann <none@none> |
moved most fundamental lemmas upwards
|
#
5531c3e2 |
|
08-Dec-2010 |
haftmann <none@none> |
bot comes before top, inf before sup etc.
|
#
78fe61a2 |
|
08-Dec-2010 |
haftmann <none@none> |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`; tuned
|
#
77c5e026 |
|
02-Dec-2010 |
hoelzl <none@none> |
Move SUP_commute, SUP_less_iff to HOL image; Cleanup generic complete_lattice lemmas in Positive_Infinite_Real; Cleanup lemma positive_integral_alt;
|
#
b1068d3f |
|
23-Nov-2010 |
hoelzl <none@none> |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
#
0bb01cdc |
|
01-Oct-2010 |
haftmann <none@none> |
constant `contents` renamed to `the_elem`
|
#
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
#
35d51202 |
|
08-Sep-2010 |
nipkow <none@none> |
put expand_(fun/set)_eq back in as synonyms, for compatibility
|
#
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
|
#
b11705e1 |
|
28-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix equality now named HOL.eq
|
#
c91cbd4e |
|
27-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
#
5f258a36 |
|
26-Aug-2010 |
haftmann <none@none> |
formerly unnamed infix impliciation now named HOL.implies
|
#
2ab2e08e |
|
25-Aug-2010 |
wenzelm <none@none> |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
#
bb1c0103 |
|
22-Aug-2010 |
blanchet <none@none> |
"no_atp" fact that leads to unsound proofs
|
#
9ee8c9cf |
|
23-Aug-2010 |
blanchet <none@none> |
"no_atp" a few facts that often lead to unsound proofs
|
#
140c6b08 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
#
b6d43d5c |
|
01-Jul-2010 |
haftmann <none@none> |
qualified constants Set.member and Set.Collect
|
#
07209de2 |
|
08-Jun-2010 |
haftmann <none@none> |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
#
43d440d9 |
|
28-Mar-2010 |
huffman <none@none> |
use lattice theorems to prove set theorems
|
#
206a5436 |
|
17-Mar-2010 |
blanchet <none@none> |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
#
86ed9410 |
|
04-Mar-2010 |
hoelzl <none@none> |
Added vimage_inter_cong
|
#
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
#
4f52a6da |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
|
#
a094de97 |
|
04-Feb-2010 |
hoelzl <none@none> |
Changed 'bounded unique existential quantifiers' from a constant to syntax translation.
|
#
7b3a0878 |
|
28-Jan-2010 |
haftmann <none@none> |
new theory Algebras.thy for generic algebraic structures
|
#
6cb03d83 |
|
30-Dec-2009 |
krauss <none@none> |
killed a few warnings
|
#
4a4d2e28 |
|
27-Nov-2009 |
berghofe <none@none> |
Removed eq_to_mono2, added not_mono.
|
#
90787a82 |
|
09-Nov-2009 |
paulson <none@none> |
New theory Probability/Borel.thy, and some associated lemmas
|
#
8de45ab6 |
|
21-Oct-2009 |
haftmann <none@none> |
dropped redundant gen_ prefix
|
#
ee2c102c |
|
20-Oct-2009 |
paulson <none@none> |
Some new lemmas concerning sets
|
#
68478f6d |
|
20-Oct-2009 |
haftmann <none@none> |
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
|
#
4f1483a7 |
|
20-Oct-2009 |
paulson <none@none> |
Removal of the unused atpset concept, the atp attribute and some related code.
|
#
45b3b64c |
|
07-Oct-2009 |
haftmann <none@none> |
tuned proofs
|
#
92ba9c59 |
|
18-Sep-2009 |
haftmann <none@none> |
inter and union are mere abbreviations for inf and sup
|
#
8163f374 |
|
31-Aug-2009 |
nipkow <none@none> |
tuned the simp rules for Int involving insert and intervals.
|
#
79c82db5 |
|
28-Jul-2009 |
haftmann <none@none> |
Set.UNIV and Set.empty are mere abbreviations for top and bot
|
#
7411135a |
|
22-Jul-2009 |
haftmann <none@none> |
moved complete_lattice &c. into separate theory --HG-- rename : src/HOL/Set.thy => src/HOL/Complete_Lattice.thy
|
#
86fbc6fe |
|
22-Jul-2009 |
haftmann <none@none> |
set intersection and union now named inter and union; closer connection between set and lattice operations; factored out complete lattice
|
#
34f0d002 |
|
21-Jul-2009 |
haftmann <none@none> |
attempt for more concise setup of non-etacontracting binders
|
#
2b61dda1 |
|
21-Jul-2009 |
haftmann <none@none> |
Set.thy: prefer = over == where possible; tuned ML setup; dropped (moved) ML legacy
|
#
fd122802 |
|
20-Jul-2009 |
haftmann <none@none> |
swapped bootstrap order of UNION/Union and INTER/Inter in theory Set
|
#
145f1294 |
|
20-Jul-2009 |
haftmann <none@none> |
less digestible
|
#
c03a97d2 |
|
20-Jul-2009 |
haftmann <none@none> |
refined outline structure
|
#
8371aa4f |
|
20-Jul-2009 |
haftmann <none@none> |
closer relation of sets and complete lattices; corresponding consts, defs and syntax at similar places in theory text
|
#
a5a5665f |
|
15-Jul-2009 |
wenzelm <none@none> |
more antiquotations;
|
#
ee1f011f |
|
14-Jul-2009 |
haftmann <none@none> |
refinement of lattice classes
|
#
822ce3cc |
|
11-Jul-2009 |
haftmann <none@none> |
added boolean_algebra type class; tuned lattice duals
|
#
d62b04dd |
|
06-Jul-2009 |
wenzelm <none@none> |
structure Thm: less pervasive names;
|
#
89539a62 |
|
15-Jun-2009 |
haftmann <none@none> |
authentic syntax for Pow and image
|
#
7451b308 |
|
04-Jun-2009 |
nipkow <none@none> |
finite lemmas
|
#
1ea3449b |
|
04-Jun-2009 |
haftmann <none@none> |
insert now qualified and with authentic syntax
|
#
457c080b |
|
18-May-2009 |
nipkow <none@none> |
fine-tuned elimination of comprehensions involving x=t.
|
#
334b16f4 |
|
16-May-2009 |
nipkow <none@none> |
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}" by the new simproc defColl_regroup. More precisely, the simproc pulls an equation x=t (or t=x) out of a nest of conjunctions to the front where the simp rule singleton_conj_conv(2) converts to "if".
|
#
0c09b37d |
|
31-Mar-2009 |
wenzelm <none@none> |
tuned;
|
#
30d86d39 |
|
19-Mar-2009 |
haftmann <none@none> |
tuned some theorem and attribute bindings
|
#
a4eb86fb |
|
13-Mar-2009 |
haftmann <none@none> |
reverted to old version of Set.thy -- strange effects have to be traced first
|
#
4def542f |
|
07-Mar-2009 |
haftmann <none@none> |
restructured theory Set.thy
|
#
bf255bf9 |
|
05-Mar-2009 |
haftmann <none@none> |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
#
ca60ee5d |
|
13-Feb-2009 |
nipkow <none@none> |
finiteness lemmas
|
#
9215e2d7 |
|
29-Jan-2009 |
berghofe <none@none> |
Added strong congruence rule for UN.
|
#
d63044b5 |
|
09-Oct-2008 |
haftmann <none@none> |
`code func` now just `code`
|
#
f8928394 |
|
11-Aug-2008 |
haftmann <none@none> |
rudimentary code setup for set operations
|
#
c69018c8 |
|
30-Jun-2008 |
huffman <none@none> |
remove simp attribute from range_composition
|
#
8a6cac34 |
|
10-Jun-2008 |
haftmann <none@none> |
removed some dubious code lemmas
|
#
8fe35509 |
|
07-May-2008 |
berghofe <none@none> |
- Now uses Orderings as parent theory - "'a set" is now just a type abbreviation for "'a => bool" - The instantiation "set :: (type) ord" and the definition of (p)subset is no longer needed, since it is subsumed by the order on functions and booleans. The derived theorems (p)subset_eq can be used as a replacement. - mem_Collect_eq and Collect_mem_eq can now be derived from the definitions of mem and Collect. - Replaced the instantiation "set :: (type) minus" by the two instantiations "fun :: (type, minus) minus" and "bool :: minus". The theorem set_diff_eq can be used as a replacement for the definition set_diff_def - Replaced the instantiation "set :: (type) uminus" by the two instantiations "fun :: (type, uminus) uminus" and "bool :: uminus". The theorem Compl_eq can be used as a replacement for the definition Compl_def. - Variable P in rule split_if must be instantiated manually in proof of split_if_mem2 due to problems with HO unification - Moved definition of dense linear orders and proofs about LEAST from Orderings to Set - Deleted code setup for sets
|
#
188a4409 |
|
22-Apr-2008 |
haftmann <none@none> |
constant HOL.eq now qualified
|
#
e2757f5b |
|
02-Apr-2008 |
haftmann <none@none> |
explicit class "eq" for operational equality
|
#
04e92685 |
|
29-Mar-2008 |
wenzelm <none@none> |
replaced 'ML_setup' by 'ML';
|
#
61320269 |
|
19-Mar-2008 |
wenzelm <none@none> |
eliminated change_claset/simpset;
|
#
add6839e |
|
26-Feb-2008 |
haftmann <none@none> |
moved some set lemmas from Set.thy here
|
#
c4bd05ca |
|
25-Jan-2008 |
haftmann <none@none> |
improved code theorem setup
|
#
16475496 |
|
02-Jan-2008 |
haftmann <none@none> |
splitted class uminus from class minus
|
#
afc0b201 |
|
30-Nov-2007 |
haftmann <none@none> |
adjustions to due to instance target
|
#
732b4c9d |
|
29-Nov-2007 |
haftmann <none@none> |
instance command as rudimentary class target
|
#
8bd9c12e |
|
23-Nov-2007 |
haftmann <none@none> |
interpretation of typedecls: instantiation to class type
|
#
952b8690 |
|
09-Nov-2007 |
krauss <none@none> |
avoid name clashes when generating code for union, inter
|
#
d95f4f2d |
|
05-Nov-2007 |
nipkow <none@none> |
added lemmas
|
#
c6fc1bb5 |
|
26-Sep-2007 |
haftmann <none@none> |
convenient obtain rule for sets
|
#
cb112997 |
|
20-Sep-2007 |
haftmann <none@none> |
clarified code lemmas
|
#
c67d4a86 |
|
24-Aug-2007 |
haftmann <none@none> |
made sets executable
|
#
1f542704 |
|
19-Aug-2007 |
nipkow <none@none> |
Made UN_Un simp
|
#
003ce27b |
|
17-Aug-2007 |
haftmann <none@none> |
dropped junk
|
#
35ae3509 |
|
14-Aug-2007 |
paulson <none@none> |
ATP blacklisting is now in theory data, attribute noatp
|
#
29547bde |
|
15-Aug-2007 |
haftmann <none@none> |
updated code generator setup
|
#
b8ec8316 |
|
20-Jul-2007 |
haftmann <none@none> |
simplified HOL bootstrap
|
#
1ab60aee |
|
19-Jul-2007 |
haftmann <none@none> |
code lemma for contents
|
#
8d82473b |
|
06-May-2007 |
haftmann <none@none> |
changed code generator invocation syntax
|
#
167fea11 |
|
20-Apr-2007 |
haftmann <none@none> |
Isar definitions are now added explicitly to code theorem table
|
#
063dbe49 |
|
20-Mar-2007 |
haftmann <none@none> |
fixed typo
|
#
e421c4a6 |
|
16-Mar-2007 |
haftmann <none@none> |
added instance of sets as distributive lattices
|
#
af98260f |
|
12-Mar-2007 |
wenzelm <none@none> |
syntax: proper body priorty for derived binders;
|
#
9e398729 |
|
28-Feb-2007 |
wenzelm <none@none> |
tuned ML setup;
|
#
c41552bd |
|
24-Jan-2007 |
paulson <none@none> |
some new lemmas
|
#
d06ce1ce |
|
20-Jan-2007 |
wenzelm <none@none> |
tuned ML setup;
|
#
fbadea40 |
|
13-Dec-2006 |
haftmann <none@none> |
dropped FIXME comment
|
#
4a92596d |
|
13-Dec-2006 |
haftmann <none@none> |
fixed syntax for bounded quantification
|
#
9f120b31 |
|
05-Dec-2006 |
wenzelm <none@none> |
removed legacy ML bindings;
|
#
49854bb1 |
|
27-Nov-2006 |
haftmann <none@none> |
restructured some proofs
|
#
b538f435 |
|
26-Nov-2006 |
wenzelm <none@none> |
updated (binder) syntax/notation;
|
#
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
#
84c0352e |
|
15-Nov-2006 |
haftmann <none@none> |
moved transitivity rules to Orderings.thy
|
#
f002ff9b |
|
13-Nov-2006 |
haftmann <none@none> |
dropped LOrder dependency
|
#
c9418c62 |
|
12-Nov-2006 |
nipkow <none@none> |
image_constant_conv no longer [simp]
|
#
ff13c87f |
|
12-Nov-2006 |
nipkow <none@none> |
started reorgnization of lattice theories
|
#
cbb1a051 |
|
07-Nov-2006 |
wenzelm <none@none> |
renamed 'const_syntax' to 'notation';
|
#
d8bb4109 |
|
14-Aug-2006 |
haftmann <none@none> |
simplified code generator setup
|
#
745db1a3 |
|
26-Jul-2006 |
webertj <none@none> |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
#
436289db |
|
13-Jun-2006 |
paulson <none@none> |
new results
|
#
61bd82ad |
|
16-May-2006 |
wenzelm <none@none> |
tuned concrete syntax -- abbreviation/const_syntax;
|
#
a347ff4a |
|
13-May-2006 |
wenzelm <none@none> |
reactivated translations for less/less_eq;
|
#
b5d7d8ec |
|
08-Apr-2006 |
wenzelm <none@none> |
refined 'abbreviation';
|
#
84161ae1 |
|
23-Mar-2006 |
nipkow <none@none> |
Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
|
#
98345ffe |
|
20-Mar-2006 |
paulson <none@none> |
subsetI is often necessary
|
#
58e4fa9b |
|
17-Mar-2006 |
haftmann <none@none> |
renamed op < <= to Orderings.less(_eq)
|
#
20f2bc8b |
|
10-Mar-2006 |
haftmann <none@none> |
renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
|
#
9ef688d7 |
|
02-Mar-2006 |
paulson <none@none> |
subset_refl now included using the atp attribute
|
#
d7c76f67 |
|
30-Jan-2006 |
haftmann <none@none> |
adaptions to codegen_package
|
#
13cda3f7 |
|
29-Jan-2006 |
wenzelm <none@none> |
declare 'defn' rules;
|
#
eaba521f |
|
13-Jan-2006 |
nipkow <none@none> |
*** empty log message ***
|
#
d9f4c279 |
|
20-Dec-2005 |
paulson <none@none> |
removed or modified some instances of [iff]
|
#
81f9ff25 |
|
16-Dec-2005 |
nipkow <none@none> |
new lemmas
|
#
63523f4e |
|
15-Dec-2005 |
wenzelm <none@none> |
removed obsolete/unused setup_induction;
|
#
a302a4ce |
|
01-Dec-2005 |
wenzelm <none@none> |
simprocs: static evaluation of simpset;
|
#
21e8c6d8 |
|
01-Dec-2005 |
paulson <none@none> |
restoring the old status of subset_refl
|
#
06d1d294 |
|
10-Nov-2005 |
paulson <none@none> |
duplicate axioms in ATP linkup, and general fixes
|
#
f7fba198 |
|
17-Oct-2005 |
wenzelm <none@none> |
change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
#
1cde857b |
|
07-Oct-2005 |
wenzelm <none@none> |
Term.absdummy;
|
#
322782fa |
|
28-Sep-2005 |
paulson <none@none> |
a name for empty_not_insert
|
#
b540c859 |
|
28-Sep-2005 |
wenzelm <none@none> |
more finalconsts;
|
#
0789ab36 |
|
22-Sep-2005 |
nipkow <none@none> |
renamed rules to iprover
|
#
112ea486 |
|
20-Sep-2005 |
wenzelm <none@none> |
tuned theory dependencies;
|
#
9dccfecd |
|
16-Aug-2005 |
paulson <none@none> |
more simprules now have names
|
#
fff82f5e |
|
16-Aug-2005 |
paulson <none@none> |
classical rules must have names for ATP integration
|
#
593d5827 |
|
02-Aug-2005 |
wenzelm <none@none> |
simprocs: Simplifier.inherit_bounds;
|
#
6265e9d3 |
|
11-Jul-2005 |
paulson <none@none> |
tweaked
|
#
58633204 |
|
01-Jul-2005 |
berghofe <none@none> |
Added strong_ball_cong and strong_bex_cong (these are now the standard congruence rules for Ball and Bex).
|
#
2f36bf40 |
|
11-May-2005 |
nipkow <none@none> |
Added thms by Brian Huffmann
|
#
2e3692ae |
|
01-Mar-2005 |
nipkow <none@none> |
integrated Jeremy's FiniteLib
|
#
5c67c68a |
|
18-Feb-2005 |
nipkow <none@none> |
tuning
|
#
14c0d9ab |
|
10-Feb-2005 |
nipkow <none@none> |
Moved oderings from HOL into the new Orderings.thy
|
#
bd899f05 |
|
27-Sep-2004 |
ballarin <none@none> |
Modified locales: improved implementation of "includes".
|
#
0fe1d442 |
|
18-Aug-2004 |
nipkow <none@none> |
import -> imports
|
#
e61c8d7d |
|
16-Aug-2004 |
nipkow <none@none> |
New theory header syntax.
|
#
4c77b830 |
|
06-Aug-2004 |
nipkow <none@none> |
undid UN/INT syntax
|
#
da2ac1c7 |
|
03-Aug-2004 |
paulson <none@none> |
new simprules Int_subset_iff and Un_subset_iff
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
873ce8ea |
|
29-May-2004 |
wenzelm <none@none> |
\<^bsub>/\<^esub> syntax: unbreakable block;
|
#
1582b657 |
|
28-May-2004 |
paulson <none@none> |
new theorem Collect_imp_eq
|
#
dace4d46 |
|
26-May-2004 |
nipkow <none@none> |
Corrected printer bug for bounded quantifiers Q x<=y. P
|
#
af2b418c |
|
17-May-2004 |
mehta <none@none> |
lemma disjoint_int_union removed - too special
|
#
fe19460e |
|
13-May-2004 |
mehta <none@none> |
New simp rules added: insert_disjoint disjoint_insert disjoint_int_union
|
#
6adc19f1 |
|
01-May-2004 |
wenzelm <none@none> |
improved subscript syntax;
|
#
cd257618 |
|
14-Apr-2004 |
kleing <none@none> |
use more symbols in HTML output
|
#
f883c383 |
|
13-Apr-2004 |
ballarin <none@none> |
Various changes to HOL-Algebra; Locale instantiation.
|
#
08d00813 |
|
24-Mar-2004 |
paulson <none@none> |
streamlined treatment of quotients for the integers
|
#
29c20de7 |
|
19-Feb-2004 |
ballarin <none@none> |
Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
|
#
44053f1b |
|
10-Feb-2004 |
nipkow <none@none> |
Modified UN and INT xsymbol syntax: made index subscript
|
#
d1e2dad4 |
|
01-Jan-2004 |
paulson <none@none> |
conversion of Real/PReal to Isar script; type "complex" is now in class "field"
|
#
51fbac88 |
|
18-Dec-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
b79b3996 |
|
26-Sep-2003 |
paulson <none@none> |
misc tidying
|
#
3ca417c4 |
|
11-Jul-2003 |
oheimb <none@none> |
added rev_ballE
|
#
9fe1e48b |
|
17-Mar-2003 |
paulson <none@none> |
moved one proof, added another
|
#
56c0192c |
|
14-Mar-2003 |
paulson <none@none> |
new UN/INT simprules
|
#
b0494754 |
|
11-Mar-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
5bd3452c |
|
26-Feb-2003 |
paulson <none@none> |
new lemma
|
#
10ff8ff5 |
|
24-Feb-2003 |
nipkow <none@none> |
Undid eta change for UN/INT.
|
#
450f9b73 |
|
15-Feb-2003 |
paulson <none@none> |
new theorem Compl_partition2
|
#
2c8d53fc |
|
22-Dec-2002 |
nipkow <none@none> |
removed some problems with print translations
|
#
130b7821 |
|
22-Dec-2002 |
nipkow <none@none> |
added print translations tha avoid eta contraction for important binders.
|
#
a55e73ba |
|
18-Oct-2002 |
nipkow <none@none> |
Added a few thms about UN/INT/{}/UNIV
|
#
b9c419c3 |
|
03-Oct-2002 |
paulson <none@none> |
added the new elim rule psubsetE
|
#
084e5d05 |
|
30-Aug-2002 |
paulson <none@none> |
removal of blast.overloaded
|
#
1f05977e |
|
06-Aug-2002 |
wenzelm <none@none> |
sane interface for simprocs;
|
#
9b541a1e |
|
24-Jul-2002 |
wenzelm <none@none> |
simplified locale predicates;
|
#
3abc26ab |
|
07-May-2002 |
wenzelm <none@none> |
rev_bexI [intro?];
|
#
d653079a |
|
06-May-2002 |
nipkow <none@none> |
Added insert_disjoint and disjoint_insert [simp], and simplified proofs
|
#
74fc2075 |
|
25-Feb-2002 |
wenzelm <none@none> |
clarified syntax of ``long'' statements: fixes/assumes/shows;
|
#
32888e81 |
|
16-Feb-2002 |
wenzelm <none@none> |
converted/deleted equalities.ML, mono.ML, subset.ML (see Set.thy);
|
#
5de92fb9 |
|
04-Jan-2002 |
wenzelm <none@none> |
tuned ``syntax (output)'';
|
#
543684e4 |
|
01-Dec-2001 |
wenzelm <none@none> |
renamed class "term" to "type" (actually "HOL.type");
|
#
de94441b |
|
20-Nov-2001 |
wenzelm <none@none> |
theory Inverse_Image converted and moved to Set;
|
#
c1694cb4 |
|
08-Nov-2001 |
wenzelm <none@none> |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
#
9868f857 |
|
02-Nov-2001 |
wenzelm <none@none> |
tuned;
|
#
8fdb03cd |
|
02-Nov-2001 |
wenzelm <none@none> |
theory Calculation move to Set;
|
#
cf8cde2e |
|
30-Oct-2001 |
wenzelm <none@none> |
lemma Least_mono moved from Typedef.thy to Set.thy;
|
#
2cf5a93d |
|
28-Oct-2001 |
wenzelm <none@none> |
converted theory "Set";
|
#
c0ed1959 |
|
14-Oct-2001 |
wenzelm <none@none> |
removed Ord;
|
#
3c6b26c9 |
|
28-Jan-2001 |
nipkow <none@none> |
fixed set comprehension print translation
|
#
ee7fa931 |
|
09-Jan-2001 |
nipkow <none@none> |
`` -> and ``` -> ``
|
#
e36e53c2 |
|
02-Oct-2000 |
wenzelm <none@none> |
range declared as syntax;
|
#
7d1af643 |
|
28-Sep-2000 |
wenzelm <none@none> |
fixed \<Union>, \<Inter> syntax;
|
#
b6c79405 |
|
28-Jan-2000 |
oheimb <none@none> |
beautified spacing for binders with symbols syntax, analogous to HOL.thy
|
#
f3125043 |
|
11-Nov-1999 |
paulson <none@none> |
new-style infix declaration for "image"
|
#
43015a92 |
|
26-Aug-1999 |
paulson <none@none> |
a little tidying; also FIXED BAD TYPE in INTER1, UNION1
|
#
064fb6c2 |
|
17-Aug-1999 |
wenzelm <none@none> |
replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);
|
#
8147eefa |
|
18-Nov-1998 |
paulson <none@none> |
Finally removing "Compl" from HOL
|
#
85471da1 |
|
30-Oct-1998 |
paulson <none@none> |
Moved "instance set:...{power} from Set.thy to RelPow.thy, where is is needed
|
#
1715bdb3 |
|
15-Sep-1998 |
paulson <none@none> |
From Compl(A) to -A
|
#
fecfc3d3 |
|
05-Aug-1998 |
paulson <none@none> |
Removal of "disjoint" translation
|
#
b0551cba |
|
04-Aug-1998 |
wenzelm <none@none> |
fixed disjount translation;
|
#
2a359397 |
|
15-Jul-1998 |
nipkow <none@none> |
Minor tidying up.
|
#
d0c6327c |
|
30-Mar-1998 |
oheimb <none@none> |
added caveat
|
#
96a93cf1 |
|
05-Nov-1997 |
paulson <none@none> |
UNIV now a constant; UNION1, INTER1 now translations and no longer have separate rules for themselves
|
#
25504a5b |
|
05-Nov-1997 |
wenzelm <none@none> |
adapted typed_print_translation;
|
#
59bbe9cb |
|
20-Oct-1997 |
wenzelm <none@none> |
adapted to qualified names;
|
#
39c87116 |
|
10-Oct-1997 |
wenzelm <none@none> |
fixed dots;
|
#
eff880c4 |
|
09-Oct-1997 |
wenzelm <none@none> |
fixed infix syntax;
|
#
b891b320 |
|
30-May-1997 |
paulson <none@none> |
Overloading of "^" requires new type class "power", with types "nat" and "set" in that class. The operator itself is declared in Nat.thy
|
#
be07250c |
|
16-May-1997 |
nipkow <none@none> |
Distributed Psubset stuff to basic set theory files, incl Finite. Added stuff by bu.
|
#
c1543ea0 |
|
16-Apr-1997 |
wenzelm <none@none> |
improved translations for subset symbols syntax: constraints;
|
#
8bb0e87a |
|
04-Apr-1997 |
nipkow <none@none> |
moved inj and surj from Set to Fun and Inv -> inv.
|
#
b8376803 |
|
25-Feb-1997 |
wenzelm <none@none> |
added proper subset symbols syntax;
|
#
b32fa5c2 |
|
16-Dec-1996 |
wenzelm <none@none> |
fixed \<subseteq> input;
|
#
08d7b5f0 |
|
13-Dec-1996 |
oheimb <none@none> |
adaptions for symbol font
|
#
6b87cf84 |
|
13-Dec-1996 |
wenzelm <none@none> |
added set inclusion symbol syntax;
|
#
48f41848 |
|
10-Dec-1996 |
wenzelm <none@none> |
fixed alternative quantifier symbol syntax;
|
#
7576ea50 |
|
10-Dec-1996 |
wenzelm <none@none> |
fixed pris of binder syntax;
|
#
d84820c6 |
|
27-Nov-1996 |
wenzelm <none@none> |
added "op :", "op ~:" syntax; added symbols syntax;
|
#
e9120bac |
|
23-Sep-1996 |
paulson <none@none> |
New infix syntax: breaks line BEFORE operator
|
#
ef827f0d |
|
09-Sep-1996 |
paulson <none@none> |
Corrected associativity: must be to right, as the type dictatess
|
#
086331a3 |
|
25-Jul-1996 |
paulson <none@none> |
Redefining "range" as a macro
|
#
741d99a4 |
|
23-Apr-1996 |
oheimb <none@none> |
*** empty log message ***
|
#
76edfd26 |
|
23-Apr-1996 |
oheimb <none@none> |
repaired critical proofs depending on the order inside non-confluent SimpSets, (temporarily) removed problematic rule less_Suc_eq form simpset_of "Nat"
|
#
79c23910 |
|
04-Mar-1996 |
nipkow <none@none> |
Added a constant UNIV == {x.True} Added many new rewrite rules for sets. Moved LEAST into Nat. Added cardinality to Finite.
|
#
53d84dbd |
|
29-Nov-1995 |
clasohm <none@none> |
removed quotes from types in consts and syntax sections
|
#
44daf58a |
|
06-Oct-1995 |
regensbu <none@none> |
added 8bit pragmas
|
#
8662ecfd |
|
22-Apr-1995 |
nipkow <none@none> |
HOL.thy: "@" is no longer introduced as a "binder" but has its own explicit translation rule "@x.b" == "Eps(%x.b)". If x is a proper pattern, further translation rules for abstractions with patterns take care of the rest. This is very modular and avoids problems with "binders" such as "!" mentioned below. let now allows pttrn (let (x,y) = t in u) instead of just idt (let x = t in u) Set.thy: UN, INT, ALL, EX, etc all use "pttrn" instead of idt. Same change as for "@" above, except that "@" was a "binder" originally. Prod.thy: Added new syntax for pttrn which allows arbitrarily nested tuples. Two translation rules take care of %pttrn. Unfortunately they cannot be reversed. Hence a little ML-code is used as well. Note that now "! (x,y). ..." is syntactically valid but leads to a translation error. This is because "!" is introduced as a "binder" which means that its translation into lambda-terms is not done by a rewrite rule (aka macro) but by some fixed ML-code which comes after the rewriting stage and does not know how to handle patterns. This looks like a minor blemish since patterns in unbounded quantifiers are not that useful (well, except maybe in unique existence ...). Ideally, there should be two syntactic categories: idts, as we know and love it, which does not admit patterns. patterns, which is what idts has become now. There is one more point where patterns are now allowed but don't make sense: {e | idts . P} where idts is the list of local variables. Univ.thy: converted the defs for <++> and <**> into pattern form. It worked perfectly.
|
#
46f10ec6 |
|
02-Mar-1995 |
clasohm <none@none> |
new version of HOL with curried function application
|