#
fe5914fe |
|
16-Feb-2020 |
nipkow <none@none> |
lemmas about "card A = 2"; prefer iff to implications
|
#
ec78305b |
|
09-Dec-2019 |
paulson <lp15@cam.ac.uk> |
a few new and tidier proofs (mostly about finite sets)
|
#
a1f8bb2d |
|
18-Sep-2019 |
paulson <lp15@cam.ac.uk> |
imported new material mostly due to Sébastien Gouëzel
|
#
453cc69e |
|
17-Apr-2019 |
paulson <lp15@cam.ac.uk> |
Lindelöf spaces and supporting material
|
#
075e0a05 |
|
01-Apr-2019 |
paulson <lp15@cam.ac.uk> |
A few results in Algebra, and bits for Analysis
|
#
ffdb775d |
|
24-Jan-2019 |
paulson <lp15@cam.ac.uk> |
the theory of Equipollence, and moving Fpow from Cardinals into Main
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
ca7063ef |
|
18-Nov-2018 |
nipkow <none@none> |
added and tuned lemmas
|
#
b9f89bc1 |
|
11-Nov-2018 |
nipkow <none@none> |
tuned
|
#
ec8d5b30 |
|
10-Nov-2018 |
haftmann <none@none> |
clarified status of legacy input abbreviations
|
#
576b136c |
|
05-Nov-2018 |
nipkow <none@none> |
simplified proof, moved lemma, added lemma
|
#
23d0d04e |
|
11-Sep-2018 |
paulson <lp15@cam.ac.uk> |
A few new results, elimination of duplicates and more use of "pairwise"
|
#
e2d96898 |
|
27-Jun-2018 |
immler <none@none> |
added lemmas and transfer rules
|
#
9e2ba9d9 |
|
18-Jun-2018 |
Lars Hupel <lars.hupel@mytum.de> |
material on finite sets and maps --HG-- extra : amend_source : ff2581f3f58668d0b07cef46bf45bbd336607dbc
|
#
ed336f6e |
|
27-Jan-2018 |
bulwahn <none@none> |
include lemmas generally useful for combinatorial proofs
|
#
acf1e346 |
|
18-Jan-2018 |
nipkow <none@none> |
moved from AFP/Gromov
|
#
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
#
0cece55a |
|
01-Oct-2016 |
wenzelm <none@none> |
tuned;
|
#
6d0b05b4 |
|
18-Sep-2016 |
wenzelm <none@none> |
tuned proofs;
|
#
2df4ddef |
|
10-Aug-2016 |
nipkow <none@none> |
"split add" -> "split"
|
#
45a0e905 |
|
05-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
65b76842 |
|
29-Jul-2016 |
Andreas Lochbihler <none@none> |
add lemmas contributed by Peter Gammie
|
#
1f8ba5d4 |
|
06-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
0f0a91d1 |
|
02-Jul-2016 |
haftmann <none@none> |
more theorems
|
#
94ba250a |
|
17-May-2016 |
eberlm <none@none> |
Moved material from AFP/Randomised_Social_Choice to distribution
|
#
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def'; tuned comments;
|
#
60a0b6b0 |
|
14-Mar-2016 |
paulson <lp15@cam.ac.uk> |
Refactoring (moving theorems into better locations), plus a bit of new material
|
#
70cb89b7 |
|
01-Mar-2016 |
haftmann <none@none> |
tuned bootstrap order to provide type classes in a more sensible order --HG-- extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
#
7b0aa853 |
|
19-Dec-2015 |
haftmann <none@none> |
abandoned attempt to unify sublocale and interpretation into global theories
|
#
474064bd |
|
09-Dec-2015 |
paulson <lp15@cam.ac.uk> |
sorted out eventually_mono
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
a17be781 |
|
03-Dec-2015 |
haftmann <none@none> |
modernized
|
#
4b76bc27 |
|
01-Dec-2015 |
paulson <lp15@cam.ac.uk> |
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
|
#
2ceb4cc9 |
|
14-Nov-2015 |
wenzelm <none@none> |
option "inductive_defs" controls exposure of def and mono facts;
|
#
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
#
8e8b881c |
|
04-Nov-2015 |
ballarin <none@none> |
Keyword 'rewrites' identifies rewrite morphisms.
|
#
b7a36669 |
|
26-Oct-2015 |
paulson <none@none> |
new lemmas about topology, etc., for Cauchy integral formula
|
#
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
#
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
#
a219c2a1 |
|
20-Jul-2015 |
paulson <none@none> |
new material for multivariate analysis, etc.
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
e2fdcde9 |
|
26-Jun-2015 |
wenzelm <none@none> |
premises in 'show' are treated like 'assume';
|
#
6f0c89b5 |
|
26-Jun-2015 |
wenzelm <none@none> |
tuned whitespace;
|
#
eb3596fa |
|
26-May-2015 |
paulson <none@none> |
New material about paths, and some lemmas
|
#
4301fc50 |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
add lema about card and vimage
|
#
b4949ab8 |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
add more general version of finite_vimageD
|
#
7145f505 |
|
10-Feb-2015 |
paulson <lp15@cam.ac.uk> |
New lemmas and a bit of tidying up.
|
#
a561406f |
|
10-Jan-2015 |
nipkow <none@none> |
added lemma
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
caa51abc |
|
06-Sep-2014 |
haftmann <none@none> |
added various facts
|
#
12022235 |
|
21-Jul-2014 |
Andreas Lochbihler <none@none> |
add lemma
|
#
6c0336e5 |
|
30-Jun-2014 |
hoelzl <none@none> |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure --HG-- extra : rebase_source : 03b2468f7b324b9d8add229ae59776b447283141
|
#
18c12fa6 |
|
20-May-2014 |
hoelzl <none@none> |
add various lemmas
|
#
12157cd1 |
|
19-Mar-2014 |
haftmann <none@none> |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
#
4f5ebd94 |
|
16-Mar-2014 |
haftmann <none@none> |
normalising simp rules for compound operators
|
#
88cc155c |
|
15-Mar-2014 |
haftmann <none@none> |
more complete set of lemmas wrt. image and composition
|
#
56332e73 |
|
21-Jan-2014 |
traytel <none@none> |
removed theory dependency of BNF_LFP on Datatype
|
#
9f589a46 |
|
20-Jan-2014 |
blanchet <none@none> |
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
|
#
c515d44a |
|
16-Jan-2014 |
blanchet <none@none> |
dissolved 'Fun_More_FP' (a BNF dependency)
|
#
d7ec4c38 |
|
28-Dec-2013 |
haftmann <none@none> |
prefix disambiguation
|
#
355cccc4 |
|
26-Dec-2013 |
haftmann <none@none> |
prefer ephemeral interpretation over interpretation in proof contexts; prefer context begin ... end blocks for often-occuring assumptions; slightly more complete interpretations into abstract algebraic structures for gcd/lcm
|
#
304043a6 |
|
29-Nov-2013 |
traytel <none@none> |
set_comprehension_pointfree simproc causes to many surprises if enabled by default
|
#
c479010b |
|
23-Nov-2013 |
paulson <none@none> |
polished some ancient proofs
|
#
67c00164 |
|
12-Nov-2013 |
hoelzl <none@none> |
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
|
#
6d11884a |
|
18-Oct-2013 |
blanchet <none@none> |
killed more "no_atp"s
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
e5a198cc |
|
24-Sep-2013 |
nipkow <none@none> |
added lemmas
|
#
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
#
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
#
18c47600 |
|
04-Apr-2013 |
haftmann <none@none> |
convenient induction rule --HG-- extra : rebase_source : 06e2fc8106aeb38db30daba81a01bbe09c008945
|
#
cef4a7ce |
|
03-Apr-2013 |
haftmann <none@none> |
generalized lemma fold_image thanks to Peter Lammich
|
#
eda70abb |
|
26-Mar-2013 |
haftmann <none@none> |
more uniform style for interpretation and sublocale declarations --HG-- extra : rebase_source : 908fa43d5ac738a6c353d74475cb1910f6a318e8
|
#
d4cae3bf |
|
23-Mar-2013 |
haftmann <none@none> |
fundamental revision of big operators on sets
|
#
a187bec2 |
|
23-Mar-2013 |
haftmann <none@none> |
locales for abstract orders
|
#
f02679c5 |
|
27-Feb-2013 |
Andreas Lochbihler <none@none> |
added lemma
|
#
8f1e3e3c |
|
10-Oct-2012 |
wenzelm <none@none> |
added some ad-hoc namespace prefixes to avoid duplicate facts;
|
#
34d50597 |
|
10-Oct-2012 |
bulwahn <none@none> |
moving simproc from Finite_Set to more appropriate Product_Type theory
|
#
69937fce |
|
09-Oct-2012 |
kuncar <none@none> |
use Set.filter instead of Finite_Set.filter, which is removed then
|
#
8f15c228 |
|
09-Oct-2012 |
kuncar <none@none> |
rename Set.project to Set.filter - more appropriate name
|
#
ff347444 |
|
07-Oct-2012 |
haftmann <none@none> |
consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common
|
#
960bd8a5 |
|
06-Oct-2012 |
haftmann <none@none> |
congruence rule for Finite_Set.fold
|
#
0af7fa0f |
|
06-Oct-2012 |
haftmann <none@none> |
alternative simplification of ^^ to the righthand side; lifting of comp_fun_commute to ^^
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
e2d0c961 |
|
01-Aug-2012 |
wenzelm <none@none> |
removed junk;
|
#
4e7f72b3 |
|
31-Jul-2012 |
kuncar <none@none> |
more set operations expressed by Finite_Set.fold
|
#
3a3e3569 |
|
03-Jul-2012 |
Andreas Lochbihler <none@none> |
add finiteness lemmas for 'a * 'b and 'a set
|
#
3ca56213 |
|
25-Jun-2012 |
wenzelm <none@none> |
tuned proofs -- prefer direct "rotated" instead of old-style COMP;
|
#
3ded6a71 |
|
25-Jun-2012 |
bulwahn <none@none> |
adding set comprehension simproc to code generation's preprocessing to generate code for some set comprehensions; noting further steps with FIXME
|
#
79d7b708 |
|
25-Jun-2012 |
wenzelm <none@none> |
ignore morphism more explicitly; tuned headers;
|
#
60fc603b |
|
20-Jun-2012 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
Integrated set comprehension pointfree simproc. --HG-- rename : src/HOL/ex/set_comprehension_pointfree.ML => src/HOL/Tools/set_comprehension_pointfree.ML
|
#
21a8723f |
|
01-Jun-2012 |
huffman <none@none> |
remove duplicate lemma card_unit in favor of Finite_Set.card_UNIV_unit
|
#
d54dcfbd |
|
30-Mar-2012 |
huffman <none@none> |
rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'
|
#
8b185804 |
|
30-Mar-2012 |
huffman <none@none> |
move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy --HG-- extra : transplant_source : 4%60%A0%BC%FE%DF%19%27%B6%DB%F9vS%7D%B6hbv%B8%8E
|
#
a3193ed0 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
#
55804831 |
|
06-Jan-2012 |
haftmann <none@none> |
incorporated various theorems from theory More_Set into corpus --HG-- extra : rebase_source : 3382b66ad31349cb7368f064c467aa4a53845dd2
|
#
b0e3086b |
|
29-Dec-2011 |
haftmann <none@none> |
qualified Finite_Set.fold
|
#
6e8928c1 |
|
24-Dec-2011 |
haftmann <none@none> |
finite type class instance for `set`
|
#
9370ce8e |
|
18-Oct-2011 |
bulwahn <none@none> |
tuned
|
#
551d75e2 |
|
13-Sep-2011 |
noschinl <none@none> |
tune proofs
|
#
7e65ae14 |
|
14-Sep-2011 |
hoelzl <none@none> |
renamed Complete_Lattices lemmas, removed legacy names
|
#
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
#
4c98af0b |
|
06-Sep-2011 |
nipkow <none@none> |
added new lemmas
|
#
dc5a080e |
|
04-Sep-2011 |
haftmann <none@none> |
tuned
|
#
b50b6583 |
|
27-Jul-2011 |
hoelzl <none@none> |
finite vimage on arbitrary domains
|
#
eb0f3940 |
|
17-Jul-2011 |
haftmann <none@none> |
moving UNIV = ... equations to their proper theories
|
#
f1b2f547 |
|
19-May-2011 |
haftmann <none@none> |
tuned proofs
|
#
bcaeee56 |
|
19-May-2011 |
haftmann <none@none> |
point-free characterization of operations on finite sets
|
#
180c955e |
|
20-May-2011 |
haftmann <none@none> |
names of fold_set locales resemble name of characteristic property more closely
|
#
db9d5355 |
|
20-May-2011 |
haftmann <none@none> |
use point-free characterization for locale fun_left_comm_idem
|
#
9e6090fb |
|
14-May-2011 |
haftmann <none@none> |
use pointfree characterisation for fold_set locale
|
#
52ec777f |
|
12-May-2011 |
haftmann <none@none> |
more uniform naming of lemma
|
#
c6dd2420 |
|
07-Apr-2011 |
haftmann <none@none> |
dropped unused lemmas; proper Isar proof
|
#
7a487b17 |
|
03-Apr-2011 |
haftmann <none@none> |
tuned proofs
|
#
9a615093 |
|
02-Apr-2011 |
haftmann <none@none> |
tuned proof
|
#
ec37399a |
|
17-Mar-2011 |
nipkow <none@none> |
tuned lemma
|
#
64269ee0 |
|
16-Mar-2011 |
nipkow <none@none> |
added lemmas
|
#
5ab5866e |
|
21-Jan-2011 |
haftmann <none@none> |
moved theorem
|
#
2a37b152 |
|
21-Jan-2011 |
haftmann <none@none> |
restructured theory; tuned proofs
|
#
6fb8be2b |
|
14-Jan-2011 |
wenzelm <none@none> |
eliminated global prems; tuned proofs;
|
#
48096e82 |
|
03-Dec-2010 |
wenzelm <none@none> |
recoded latin1 as utf8; use textcomp for some text symbols where it appears appropriate;
|
#
ab64cc35 |
|
03-Dec-2010 |
bulwahn <none@none> |
adding code equation for finiteness of finite types
|
#
9e4cf179 |
|
28-Nov-2010 |
nipkow <none@none> |
gave more standard finite set rules simp and intro attribute
|
#
4afd4cef |
|
26-Nov-2010 |
nipkow <none@none> |
new lemma
|
#
b1068d3f |
|
23-Nov-2010 |
hoelzl <none@none> |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
#
b97be2fb |
|
22-Nov-2010 |
hoelzl <none@none> |
Replace surj by abbreviation; remove surj_on.
|
#
285c6c89 |
|
03-Nov-2010 |
nipkow <none@none> |
removed assumption
|
#
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
#
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
|
#
5e686b64 |
|
13-Aug-2010 |
haftmann <none@none> |
import swap prevents strange failure of SML code generator for datatypes
|
#
5e72e9aa |
|
12-Jul-2010 |
haftmann <none@none> |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
#
140c6b08 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
#
53a0b22e |
|
01-Jul-2010 |
haftmann <none@none> |
"prod" and "sum" replace "*" and "+" respectively
|
#
6fd2e29d |
|
18-Jun-2010 |
nipkow <none@none> |
added pigeonhole lemmas
|
#
31c0b027 |
|
04-May-2010 |
haftmann <none@none> |
avoid if on rhs of default simp rules
|
#
4f324f64 |
|
04-May-2010 |
haftmann <none@none> |
locale predicates of classes carry a mandatory "class" prefix
|
#
82fe7ca2 |
|
16-Apr-2010 |
wenzelm <none@none> |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
#
2ccc1ad8 |
|
07-Apr-2010 |
Christian Urban <urbanc@in.tum.de> |
simplified induction case in finite_psubset_induct; tuned the proof that uses this induction principle
|
#
b743e0a9 |
|
30-Mar-2010 |
huffman <none@none> |
simplify fold_graph proofs
|
#
29f2802b |
|
18-Mar-2010 |
haftmann <none@none> |
added locales folding_one_(idem); various streamlining and tuning
|
#
206a5436 |
|
17-Mar-2010 |
blanchet <none@none> |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
#
e1dda51b |
|
15-Mar-2010 |
haftmann <none@none> |
corrected disastrous syntax declarations
|
#
b4e8c6ae |
|
11-Mar-2010 |
haftmann <none@none> |
moved cardinality to Finite_Set as far as appropriate; added locales for fold_image
|
#
6abf497b |
|
10-Mar-2010 |
haftmann <none@none> |
split off theory Big_Operators from theory Finite_Set --HG-- rename : src/HOL/Finite_Set.thy => src/HOL/Big_Operators.thy
|
#
145cc120 |
|
04-Mar-2010 |
hoelzl <none@none> |
Generalized setsum_cases
|
#
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
#
3aa9f578 |
|
19-Feb-2010 |
haftmann <none@none> |
moved remaning class operations from Algebras.thy to Groups.thy
|
#
aaaa7964 |
|
18-Feb-2010 |
huffman <none@none> |
get rid of many duplicate simp rule warnings
|
#
fb95c91e |
|
17-Feb-2010 |
hoelzl <none@none> |
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
|
#
4f52a6da |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
|
#
b3e1c14b |
|
08-Feb-2010 |
haftmann <none@none> |
added lemmas involving Min, Max, uminus
|
#
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
#
91dc9df8 |
|
01-Jan-2010 |
nipkow <none@none> |
added lemmas
|
#
e424d6e1 |
|
17-Dec-2009 |
paulson <none@none> |
Two new theorems about cardinality
|
#
216e5fab |
|
17-Dec-2009 |
huffman <none@none> |
add lemmas rev_finite_subset, finite_vimageD, finite_vimage_iff
|
#
496367cb |
|
05-Dec-2009 |
haftmann <none@none> |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
#
b111bcd3 |
|
25-Nov-2009 |
haftmann <none@none> |
tuned --HG-- extra : rebase_source : e260d697b790839af7519c59bc99073d646fffe9
|
#
bacdb650 |
|
13-Nov-2009 |
nipkow <none@none> |
renamed lemmas "anti_sym" -> "antisym"
|
#
54e22e45 |
|
04-Nov-2009 |
nipkow <none@none> |
fixed order of parameters in induction rules
|
#
179dc521 |
|
22-Oct-2009 |
nipkow <none@none> |
inv_onto -> inv_into
|
#
def242e4 |
|
17-Oct-2009 |
nipkow <none@none> |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
354f7146 |
|
24-Sep-2009 |
haftmann <none@none> |
idempotency case for fold1
|
#
4a2205ac |
|
23-Sep-2009 |
haftmann <none@none> |
inf/sup_absorb are no default simp rules any longer
|
#
122eebc6 |
|
22-Sep-2009 |
haftmann <none@none> |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
#
92ba9c59 |
|
18-Sep-2009 |
haftmann <none@none> |
inter and union are mere abbreviations for inf and sup
|
#
10337e68 |
|
28-Aug-2009 |
nipkow <none@none> |
tuned proofs
|
#
49988048 |
|
25-Jul-2009 |
haftmann <none@none> |
adapted to localized interpretation of min/max-lattice
|
#
46908f78 |
|
15-Jul-2009 |
nipkow <none@none> |
More finite set induction rules
|
#
ee1f011f |
|
14-Jul-2009 |
haftmann <none@none> |
refinement of lattice classes
|
#
714ede60 |
|
12-Jul-2009 |
nipkow <none@none> |
typo
|
#
cc85a61a |
|
12-Jul-2009 |
nipkow <none@none> |
More about gcd/lcm, and some cleaning up
|
#
822ce3cc |
|
11-Jul-2009 |
haftmann <none@none> |
added boolean_algebra type class; tuned lattice duals
|
#
903c05f1 |
|
02-Jul-2009 |
wenzelm <none@none> |
recovered subscripts, which were lost in b41d61c768e2 (due to Emacs accident?);
|
#
67864f86 |
|
23-Jun-2009 |
haftmann <none@none> |
lemma finite_image_set by Jeremy Avigad
|
#
ac3e2f0d |
|
18-Jun-2009 |
paulson <none@none> |
Removed unnecessary conditions concerning nonzero divisors
|
#
03051661 |
|
05-Jun-2009 |
nipkow <none@none> |
new lemma
|
#
7451b308 |
|
04-Jun-2009 |
nipkow <none@none> |
finite lemmas
|
#
cad19c87 |
|
04-Jun-2009 |
haftmann <none@none> |
lemmas about basic set operations and Finite_Set.fold
|
#
41260d9c |
|
04-Jun-2009 |
nipkow <none@none> |
A few finite lemmas
|
#
29ed20ca |
|
02-Jun-2009 |
haftmann <none@none> |
added/moved lemmas by Andreas Lochbihler
|
#
6ca1bd25 |
|
08-May-2009 |
nipkow <none@none> |
lemmas by Andreas Lochbihler
|
#
baadc210 |
|
28-Apr-2009 |
haftmann <none@none> |
stripped class recpower further
|
#
6849d90e |
|
03-Apr-2009 |
nipkow <none@none> |
Finite_Set: lemma IsarRef: attribute arith
|
#
a8ac4ce1 |
|
03-Apr-2009 |
nipkow <none@none> |
added setsum_eq_1_iff
|
#
2fe1bdcf |
|
01-Apr-2009 |
nipkow <none@none> |
cleaned up setprod_zero-related lemmas
|
#
50fcaf03 |
|
01-Apr-2009 |
huffman <none@none> |
generalized setprod_nonneg and setprod_pos to ordered_semidom, simplified proofs
|
#
b69bee28 |
|
01-Apr-2009 |
nipkow <none@none> |
added strong_setprod_cong[cong] (in analogy with setsum) added some lemmas
|
#
0761d736 |
|
26-Mar-2009 |
wenzelm <none@none> |
interpretation/interpret: prefixes are mandatory by default;
|
#
cc77f959 |
|
06-Mar-2009 |
haftmann <none@none> |
equalities for Min, Max
|
#
9267164c |
|
04-Mar-2009 |
chaieb <none@none> |
Added general theorems for fold_image, setsum and set_prod
|
#
c440cf75 |
|
18-Feb-2009 |
haftmann <none@none> |
reverted to previous version of Finite_Set.thy
|
#
e357e148 |
|
18-Feb-2009 |
paulson <none@none> |
No idea what happened here!
|
#
0c95fb5b |
|
15-Feb-2009 |
nipkow <none@none> |
dvd and setprod lemmas
|
#
ad28f38f |
|
15-Feb-2009 |
nipkow <none@none> |
added finite_set_choice
|
#
bc1b7712 |
|
15-Feb-2009 |
nipkow <none@none> |
more finiteness
|
#
9b596593 |
|
14-Feb-2009 |
nipkow <none@none> |
more finiteness
|
#
58c05d0d |
|
14-Feb-2009 |
nipkow <none@none> |
more finiteness
|
#
5a0c22c6 |
|
14-Feb-2009 |
nipkow <none@none> |
more finiteness changes
|
#
ca60ee5d |
|
13-Feb-2009 |
nipkow <none@none> |
finiteness lemmas
|
#
db02b24a |
|
12-Feb-2009 |
nipkow <none@none> |
Moved FTA into Lib and cleaned it up a little. --HG-- rename : src/HOL/Fundamental_Theorem_Algebra.thy => src/HOL/Library/Fundamental_Theorem_Algebra.thy
|
#
6172af0a |
|
03-Feb-2009 |
haftmann <none@none> |
handling type classes without parameters
|
#
abf397f0 |
|
28-Jan-2009 |
nipkow <none@none> |
Replaced group_ and ring_simps by algebra_simps; removed compare_rls - use algebra_simps now
|
#
53d85601 |
|
28-Jan-2009 |
chaieb <none@none> |
Added theorems setsum_reindex_nonzero, setsum_mono_zero_left, setsum_mono_zero_right, setsum_mono_zero_cong_left, setsum_mono_zero_cong_right, setsum_delta, strong_setprod_reindex_cong, setprod_delta
|
#
73d9a35c |
|
21-Jan-2009 |
haftmann <none@none> |
changed import hierarchy
|
#
0248177c |
|
21-Jan-2009 |
haftmann <none@none> |
dropped ID
|
#
7b4d17c7 |
|
16-Jan-2009 |
haftmann <none@none> |
migrated class package to new locale implementation
|
#
6d30ce6c |
|
11-Dec-2008 |
ballarin <none@none> |
Conversion of HOL-Main and ZF to new locales.
|
#
b58a4a1b |
|
09-Dec-2008 |
huffman <none@none> |
move lemmas from Numeral_Type.thy to other theories
|
#
11e6b93b |
|
19-Nov-2008 |
nipkow <none@none> |
Added new fold operator and renamed the old oe to fold_image.
|
#
39d5f60f |
|
17-Nov-2008 |
haftmann <none@none> |
tuned unfold_locales invocation
|
#
f3b50129 |
|
24-Aug-2008 |
haftmann <none@none> |
tuned import order
|
#
38e69d61 |
|
15-Jul-2008 |
ballarin <none@none> |
Removed uses of context element includes.
|
#
a2a98cd2 |
|
01-Jul-2008 |
huffman <none@none> |
prove lemma finite in context of finite class
|
#
c69018c8 |
|
30-Jun-2008 |
huffman <none@none> |
remove simp attribute from range_composition
|
#
f42f96c3 |
|
12-Jun-2008 |
nipkow <none@none> |
Hid swap
|
#
efd9fcbd |
|
07-May-2008 |
berghofe <none@none> |
- Deleted code setup for finite and card - Deleted proof of "instance set :: (finite) finite" and modified proof of "instance fun :: (finite, finite) finite", which now uses some ideas from the instance proof for sets - Instantiated arg_cong rule to avoid problems with HO unification
|
#
5c0acccf |
|
28-Apr-2008 |
haftmann <none@none> |
thms Max_ge, Min_le: dropped superfluous premise
|
#
ee5945c1 |
|
25-Apr-2008 |
krauss <none@none> |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
#
257520ee |
|
28-Mar-2008 |
haftmann <none@none> |
only invoke interpret
|
#
fd196c57 |
|
27-Mar-2008 |
haftmann <none@none> |
no "attach UNIV" any more
|
#
20954845 |
|
26-Feb-2008 |
haftmann <none@none> |
tuned proofs
|
#
6d7695b0 |
|
06-Feb-2008 |
haftmann <none@none> |
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
|
#
c8abed18 |
|
07-Dec-2007 |
haftmann <none@none> |
instantiation target rather than legacy instance
|
#
732b4c9d |
|
29-Nov-2007 |
haftmann <none@none> |
instance command as rudimentary class target
|
#
a1db5318 |
|
23-Nov-2007 |
haftmann <none@none> |
deleted card definition as code lemma; authentic syntax for card
|
#
7a7f611b |
|
06-Nov-2007 |
haftmann <none@none> |
renamed lordered_*_* to lordered_*_add_*; further localization
|
#
a9af894e |
|
26-Oct-2007 |
haftmann <none@none> |
dropped "brown" syntax
|
#
002c9527 |
|
23-Oct-2007 |
nipkow <none@none> |
went back to >0
|
#
d2ad869d |
|
16-Oct-2007 |
haftmann <none@none> |
global class syntax
|
#
379c3a11 |
|
15-Oct-2007 |
haftmann <none@none> |
explicit parameter for class finite
|
#
ba948713 |
|
08-Oct-2007 |
haftmann <none@none> |
clarified
|
#
02b407a9 |
|
05-Oct-2007 |
nipkow <none@none> |
added lemmas
|
#
62ee215f |
|
29-Sep-2007 |
haftmann <none@none> |
proper syntax during class specification
|
#
c65e27dd |
|
26-Sep-2007 |
haftmann <none@none> |
moved Finite_Set before Datatype
|
#
2a6f8876 |
|
20-Sep-2007 |
haftmann <none@none> |
code lemmas for cardinality
|
#
b658a19b |
|
15-Sep-2007 |
haftmann <none@none> |
added lemmas for finiteness
|
#
29b6546d |
|
24-Aug-2007 |
paulson <none@none> |
revised blacklisting for ATP linkup
|
#
6c756428 |
|
21-Aug-2007 |
haftmann <none@none> |
moved ordered_ab_semigroup_add to OrderedGroup.thy
|
#
ac7890e0 |
|
20-Aug-2007 |
haftmann <none@none> |
conciliated Inf/Inf_fin
|
#
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
|
#
e66904a4 |
|
14-Aug-2007 |
huffman <none@none> |
minimize imports
|
#
76d20c1a |
|
14-Aug-2007 |
huffman <none@none> |
rename lemmas finite->finite_UNIV, finite_set->finite; declare finite[simp]
|
#
61bc019f |
|
09-Aug-2007 |
haftmann <none@none> |
re-eliminated Option.thy
|
#
6c86ca52 |
|
07-Aug-2007 |
haftmann <none@none> |
simplified proofs
|
#
0a5df459 |
|
24-Jul-2007 |
haftmann <none@none> |
using interpretation with derived concepts
|
#
b8ec8316 |
|
20-Jul-2007 |
haftmann <none@none> |
simplified HOL bootstrap
|
#
e6606bce |
|
11-Jul-2007 |
berghofe <none@none> |
Renamed inductive2 to inductive.
|
#
14e11613 |
|
10-Jul-2007 |
haftmann <none@none> |
moved some finite lemmas here
|
#
b48ec05b |
|
23-Jun-2007 |
nipkow <none@none> |
tuned and renamed group_eq_simps and ring_eq_simps
|
#
d3f721d9 |
|
17-Jun-2007 |
nipkow <none@none> |
tuned laws for cancellation in divisions for fields.
|
#
2bd57634 |
|
15-Jun-2007 |
nipkow <none@none> |
made divide_self a simp rule
|
#
282fc2bd |
|
14-Jun-2007 |
wenzelm <none@none> |
tuned proofs: avoid implicit prems;
|
#
f2d5bcde |
|
06-Jun-2007 |
huffman <none@none> |
generalize class constraints on some lemmas
|
#
36841023 |
|
04-Jun-2007 |
haftmann <none@none> |
tuned comments
|
#
0263c30e |
|
24-May-2007 |
haftmann <none@none> |
rudimentary class target implementation
|
#
0a32d854 |
|
19-May-2007 |
haftmann <none@none> |
no special treatment in naming of locale predicates stemming form classes
|
#
1ee540b7 |
|
11-May-2007 |
nipkow <none@none> |
*** empty log message ***
|
#
257a782a |
|
10-May-2007 |
huffman <none@none> |
generalize setsum lemmas from semiring_0_cancel to semiring_0
|
#
5edc5dfe |
|
10-May-2007 |
haftmann <none@none> |
localized Min/Max
|
#
23d044a2 |
|
09-Apr-2007 |
huffman <none@none> |
generalized type of lemma setsum_product
|
#
5df90403 |
|
20-Mar-2007 |
haftmann <none@none> |
explizit "type" superclass
|
#
4a87e566 |
|
16-Mar-2007 |
haftmann <none@none> |
added FIXME hints
|
#
ffe2c1fc |
|
09-Mar-2007 |
haftmann <none@none> |
moved order on functions here
|
#
db5566f4 |
|
03-Mar-2007 |
haftmann <none@none> |
moved instance option :: finite here
|
#
e62f0535 |
|
02-Mar-2007 |
haftmann <none@none> |
added code theorems for UNIV
|
#
54c1e076 |
|
14-Feb-2007 |
haftmann <none@none> |
added class "preorder"
|
#
1daf9028 |
|
07-Feb-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
#
04d897fa |
|
09-Dec-2006 |
nipkow <none@none> |
Modified lattice locale
|
#
d309d4cd |
|
02-Dec-2006 |
haftmann <none@none> |
generalized type signature of foldSet, fold
|
#
f695917d |
|
28-Nov-2006 |
wenzelm <none@none> |
tuned proofs;
|
#
d43d22ca |
|
17-Nov-2006 |
haftmann <none@none> |
clarified module dependencies
|
#
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
#
349620b1 |
|
08-Nov-2006 |
haftmann <none@none> |
renamed Lattice_Locales to Lattices
|
#
76fbe45c |
|
07-Nov-2006 |
haftmann <none@none> |
made locale partial_order compatible with axclass order
|
#
7c6dcf67 |
|
07-Nov-2006 |
krauss <none@none> |
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0. Richer structures do not inherit from semiring_0 anymore, because anihilation is a theorem there, not an axiom. * Generalized axclass "recpower" to arbitrary monoid, not just commutative semirings.
|
#
50485331 |
|
04-Jul-2006 |
ballarin <none@none> |
Method intro_locales replaced by intro_locales and unfold_locales.
|
#
0c7ce443 |
|
20-Jun-2006 |
ballarin <none@none> |
Restructured locales with predicates: import is now an interpretation. New method intro_locales.
|
#
436289db |
|
13-Jun-2006 |
paulson <none@none> |
new results
|
#
ebc24da3 |
|
12-Jun-2006 |
wenzelm <none@none> |
tuned;
|
#
89c54ad9 |
|
06-Jun-2006 |
paulson <none@none> |
new lemmas concerning finite cardinalities
|
#
1e566d0d |
|
02-May-2006 |
wenzelm <none@none> |
replaced syntax/translations by abbreviation; tuned proofs; tuned;
|
#
b5d7d8ec |
|
08-Apr-2006 |
wenzelm <none@none> |
refined 'abbreviation';
|
#
78974e35 |
|
22-Mar-2006 |
nipkow <none@none> |
translations -> abbreviations (a cool feature)
|
#
ba4ed7ee |
|
17-Mar-2006 |
ballarin <none@none> |
Renamed setsum_mult to setsum_right_distrib.
|
#
d812e8a8 |
|
22-Dec-2005 |
nipkow <none@none> |
more lemmas
|
#
81f9ff25 |
|
16-Dec-2005 |
nipkow <none@none> |
new lemmas
|
#
c046356e |
|
07-Oct-2005 |
wenzelm <none@none> |
replaced _K by dummy abstraction;
|
#
b5508303 |
|
04-Oct-2005 |
nipkow <none@none> |
new lemmas
|
#
0789ab36 |
|
22-Sep-2005 |
nipkow <none@none> |
renamed rules to iprover
|
#
b12e7272 |
|
29-Aug-2005 |
paulson <none@none> |
patterns in setsum and setprod
|
#
34682e42 |
|
26-Aug-2005 |
ballarin <none@none> |
Lemmas on dvd, power and finite summation added or strengthened.
|
#
9dccfecd |
|
16-Aug-2005 |
paulson <none@none> |
more simprules now have names
|
#
34443f9c |
|
04-Aug-2005 |
nipkow <none@none> |
added Brian Hufmann's finite instances
|
#
858431e5 |
|
12-Jul-2005 |
avigad <none@none> |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities) added lemmas to Ring_and_Field.thy (reasoning about signs, fractions, etc.) renamed simplification rules for abs (abs_of_pos, etc.) renamed rules for multiplication and signs (mult_pos_pos, etc.) moved lemmas involving fractions from NatSimprocs.thy added setsum_mono3 to FiniteSet.thy added simplification rules for powers to Parity.thy
|
#
e20e6219 |
|
08-Jul-2005 |
nipkow <none@none> |
changed imports due to new GCD.thy
|
#
9ce84e7b |
|
06-Jul-2005 |
nipkow <none@none> |
linear arithmetic now takes "&" in assumptions apart.
|
#
7704e2ed |
|
01-Jul-2005 |
berghofe <none@none> |
Added strong_setsum_cong and strong_setprod_cong.
|
#
fa115045 |
|
23-Jun-2005 |
nipkow <none@none> |
fixed \<Prod> syntax
|
#
07401353 |
|
25-Apr-2005 |
ballarin <none@none> |
Subsumption of locale interpretations.
|
#
fcd8ade1 |
|
21-Apr-2005 |
nipkow <none@none> |
tuning locales
|
#
2e3a4bca |
|
20-Apr-2005 |
nipkow <none@none> |
Used locale interpretations everywhere.
|
#
7279f29d |
|
19-Apr-2005 |
paulson <none@none> |
fixed presentation
|
#
c3c2dfe7 |
|
18-Apr-2005 |
ballarin <none@none> |
Cleaned up, now uses interpretation.
|
#
2e3692ae |
|
01-Mar-2005 |
nipkow <none@none> |
integrated Jeremy's FiniteLib
|
#
1c44df95 |
|
28-Feb-2005 |
obua <none@none> |
added setsum_diff1' which holds in more general cases than setsum_diff1
|
#
342923f0 |
|
22-Feb-2005 |
nipkow <none@none> |
more setsum tuning
|
#
dd0123f5 |
|
21-Feb-2005 |
nipkow <none@none> |
more fine tuniung
|
#
6d9b3eb2 |
|
21-Feb-2005 |
nipkow <none@none> |
comprehensive cleanup, replacing sumr by setsum
|
#
5c67c68a |
|
18-Feb-2005 |
nipkow <none@none> |
tuning
|
#
090a1e72 |
|
14-Feb-2005 |
paulson <none@none> |
simplified a proof
|
#
ba8e48fe |
|
10-Feb-2005 |
nipkow <none@none> |
some stuff is now redundant.
|
#
bc312066 |
|
10-Feb-2005 |
paulson <none@none> |
non-inductive fold1Set proofs
|
#
2ebe2cbf |
|
10-Feb-2005 |
paulson <none@none> |
simplified a key lemma for foldSet
|
#
82173bd6 |
|
10-Feb-2005 |
berghofe <none@none> |
Subscripts for theorem lists now start at 1.
|
#
e17d1a4d |
|
09-Feb-2005 |
nipkow <none@none> |
Extracted generic lattice stuff to new Lattice_Locales.thy
|
#
a0c5c7ad |
|
09-Feb-2005 |
paulson <none@none> |
new foldSet proofs
|
#
972bf364 |
|
08-Feb-2005 |
paulson <none@none> |
revised fold1 proofs
|
#
e97b56b5 |
|
09-Feb-2005 |
paulson <none@none> |
revised fold1 proofs
|
#
73671958 |
|
08-Feb-2005 |
nipkow <none@none> |
cvs merge problem fixed
|
#
774d18f1 |
|
08-Feb-2005 |
paulson <none@none> |
new treatment of fold1
|
#
aced08c8 |
|
08-Feb-2005 |
nipkow <none@none> |
Fixed lattice defns
|
#
f7bcb366 |
|
07-Feb-2005 |
nipkow <none@none> |
*** empty log message ***
|
#
2525668a |
|
07-Feb-2005 |
nipkow <none@none> |
fixed latex problems
|
#
09b4f2d7 |
|
05-Feb-2005 |
nipkow <none@none> |
Added Lattice locale
|
#
78adc55b |
|
04-Feb-2005 |
paulson <none@none> |
comment
|
#
0a5e5629 |
|
04-Feb-2005 |
nipkow <none@none> |
Added semi-lattice locales and reorganized fold1 lemmas
|
#
db7ef18b |
|
02-Feb-2005 |
paulson <none@none> |
generalization and tidying
|
#
61484b18 |
|
02-Feb-2005 |
nipkow <none@none> |
fold and fol1 changes
|
#
ef8f7250 |
|
02-Feb-2005 |
nipkow <none@none> |
added [simp]
|
#
93e84db7 |
|
30-Jan-2005 |
nipkow <none@none> |
renamed a few vars, added a lemma
|
#
d47044c3 |
|
28-Jan-2005 |
nipkow <none@none> |
proof simpification
|
#
4b1dc317 |
|
21-Jan-2005 |
paulson <none@none> |
new theorem image_eq_fold
|
#
c8d6566d |
|
14-Dec-2004 |
paulson <none@none> |
new and stronger lemmas and improved simplification for finite sets
|
#
77626512 |
|
12-Dec-2004 |
nipkow <none@none> |
REorganized Finite_Set
|
#
4fe6092b |
|
09-Dec-2004 |
nipkow <none@none> |
First step in reorganizing Finite_Set
|
#
7b56d1c7 |
|
06-Dec-2004 |
nipkow <none@none> |
Started to clean up and generalize FiniteSet
|
#
8607c133 |
|
24-Nov-2004 |
nipkow <none@none> |
changed the order of !!-quantifiers in finite set induction. In Isar you can now write (insert x F) rather than the counterintuitive (insert F x).
|
#
78092f12 |
|
23-Nov-2004 |
obua <none@none> |
prettier proof of setsum_diff
|
#
fee3a1b3 |
|
23-Nov-2004 |
nipkow <none@none> |
renamed 2 lemmas
|
#
70bb886e |
|
23-Nov-2004 |
obua <none@none> |
relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
|
#
2c603b15 |
|
23-Nov-2004 |
obua <none@none> |
Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff
|
#
a16f9adc |
|
23-Nov-2004 |
nipkow <none@none> |
generalized lemma
|
#
355d2fcd |
|
23-Nov-2004 |
nipkow <none@none> |
added lemma
|
#
51932445 |
|
12-Nov-2004 |
nipkow <none@none> |
More lemmas
|
#
2756a8fa |
|
07-Oct-2004 |
paulson <none@none> |
simplification tweaks for better arithmetic reasoning
|
#
664518d4 |
|
04-Oct-2004 |
paulson <none@none> |
revised simprules for division
|
#
0fe1d442 |
|
18-Aug-2004 |
nipkow <none@none> |
import -> imports
|
#
e61c8d7d |
|
16-Aug-2004 |
nipkow <none@none> |
New theory header syntax.
|
#
e7abad4b |
|
09-Aug-2004 |
nipkow <none@none> |
Aded a thm.
|
#
f2fa5ea3 |
|
04-Aug-2004 |
nipkow <none@none> |
added some inj_on thms
|
#
7ebc34e1 |
|
22-Jul-2004 |
nipkow <none@none> |
Modified \<Sum> syntax a little.
|
#
eb9e4051 |
|
15-Jul-2004 |
paulson <none@none> |
redefining sumr to be a translation to setsum
|
#
39278df5 |
|
14-Jul-2004 |
nipkow <none@none> |
added {0::nat..n(} = {..n(}
|
#
d2d099b3 |
|
24-Jun-2004 |
paulson <none@none> |
ringpower to recpower
|
#
833164cc |
|
15-Jun-2004 |
paulson <none@none> |
strengthened some theorems
|
#
40765332 |
|
09-Jun-2004 |
paulson <none@none> |
moved some cardinality results into main HOL
|
#
38cc1f66 |
|
14-May-2004 |
paulson <none@none> |
removed a premise of card_inj_on_le
|
#
ea2cbc80 |
|
12-May-2004 |
nipkow <none@none> |
fixed latex problems
|
#
47b52a8a |
|
11-May-2004 |
obua <none@none> |
changes made due to new Ring_and_Field theory
|
#
ef887dff |
|
23-Apr-2004 |
wenzelm <none@none> |
tuned notation;
|
#
cd257618 |
|
14-Apr-2004 |
kleing <none@none> |
use more symbols in HTML output
|
#
68eabd1d |
|
01-Apr-2004 |
paulson <none@none> |
new type class abelian_group
|
#
9a343c34 |
|
25-Mar-2004 |
paulson <none@none> |
new material from Avigad
|
#
aafa34f4 |
|
10-Mar-2004 |
paulson <none@none> |
strengthened the axclass claims
|
#
f281a512 |
|
08-Mar-2004 |
paulson <none@none> |
generic theorems about exponentials; general tidying up
|
#
30ab08fd |
|
03-Mar-2004 |
paulson <none@none> |
new material from Avigad, and simplified treatment of division by 0
|
#
1f556718 |
|
27-Dec-2003 |
paulson <none@none> |
re-organized numeric lemmas
|
#
51fbac88 |
|
18-Dec-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
b79b3996 |
|
26-Sep-2003 |
paulson <none@none> |
misc tidying
|
#
4da2b933 |
|
20-Feb-2003 |
paulson <none@none> |
new inverse image lemmas
|
#
9255c907 |
|
29-Nov-2002 |
nipkow <none@none> |
added a few lemmas
|
#
57e3f1ba |
|
28-Nov-2002 |
ballarin <none@none> |
HOL-Algebra partially ported to Isar.
|
#
aa4aa83c |
|
13-Nov-2002 |
berghofe <none@none> |
Transitive closure is now defined inductively as well.
|
#
55720395 |
|
27-Sep-2002 |
paulson <none@none> |
Proof tidying
|
#
573a0671 |
|
20-Sep-2002 |
paulson <none@none> |
less use of x-symbols
|
#
94df863f |
|
12-Aug-2002 |
nipkow <none@none> |
Added Mi and Max on sets, hid Min and Pls on numerals.
|
#
9b541a1e |
|
24-Jul-2002 |
wenzelm <none@none> |
simplified locale predicates;
|
#
0e2734b6 |
|
19-Jul-2002 |
wenzelm <none@none> |
accomodate cumulative locale predicates;
|
#
3f59774e |
|
17-Jul-2002 |
wenzelm <none@none> |
ACe_axioms;
|
#
aa4dd3c8 |
|
16-Jul-2002 |
wenzelm <none@none> |
adapted to locale defs;
|
#
74fc2075 |
|
25-Feb-2002 |
wenzelm <none@none> |
clarified syntax of ``long'' statements: fixes/assumes/shows;
|
#
7bab8973 |
|
11-Jan-2002 |
wenzelm <none@none> |
lemmas (in ACe) AC;
|
#
d6035b54 |
|
09-Jan-2002 |
wenzelm <none@none> |
qualified exports from locales;
|
#
2d4125ec |
|
05-Dec-2001 |
wenzelm <none@none> |
renamed theory Finite to Finite_Set and converted;
|