| #
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
|
| #
6effda26 |
|
14-Jan-2019 |
nipkow <none@none> |
uniform naming
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
6fd6219b |
|
21-Oct-2018 |
nipkow <none@none> |
uniform naming of strong congruence rules
|
| #
9e2ba9d9 |
|
18-Jun-2018 |
Lars Hupel <lars.hupel@mytum.de> |
material on finite sets and maps
--HG--
extra : amend_source : ff2581f3f58668d0b07cef46bf45bbd336607dbc
|
| #
965df47d |
|
12-Mar-2018 |
Manuel Eberl <eberlm@in.tum.de> |
Changes to complete distributive lattices due to Viorel Preoteasa
|
| #
c0a19014 |
|
03-Mar-2018 |
ballarin <none@none> |
Drop rewrites after defines in interpretations.
|
| #
39994669 |
|
12-Jan-2018 |
wenzelm <none@none> |
prefer formal comments;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
35c0f2a1 |
|
20-Jul-2017 |
Lars Hupel <lars.hupel@mytum.de> |
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
|
| #
94deaba7 |
|
11-Jul-2017 |
Lars Hupel <lars.hupel@mytum.de> |
card_0_eq ~> fcard_0_eq
|
| #
c71d441c |
|
11-Jul-2017 |
Lars Hupel <lars.hupel@mytum.de> |
material from $AFP/Formula_Derivatives/FSet_More
|
| #
9592ed4f |
|
10-Jul-2017 |
Lars Hupel <lars.hupel@mytum.de> |
finite sets are countable
--HG--
extra : amend_source : cea729a1e159fa171d76020f2bccdb82281d87dc
|
| #
8b016743 |
|
10-Jul-2017 |
Lars Hupel <lars.hupel@mytum.de> |
lift sum to finite sets
|
| #
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
| #
0bd59400 |
|
10-Aug-2016 |
wenzelm <none@none> |
tuned proofs;
|
| #
8b97f94a |
|
06-Aug-2016 |
Lars Hupel <lars.hupel@mytum.de> |
some additions to FSet
|
| #
48473ab7 |
|
22-Jun-2016 |
wenzelm <none@none> |
bundle lifting_syntax;
|
| #
13683eca |
|
17-Jun-2016 |
hoelzl <none@none> |
move Conditional_Complete_Lattices to Main
--HG--
extra : rebase_source : 2cd0f07680d0081b5d3769e8a4ad49983a312a99
|
| #
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
6b18406f |
|
16-Feb-2016 |
traytel <none@none> |
make predicator a first-class bnf citizen
|
| #
8b08bf14 |
|
07-Jan-2016 |
paulson <none@none> |
revisions to limits and derivatives, plus new lemmas
|
| #
95681996 |
|
06-Jan-2016 |
blanchet <none@none> |
nicer 'Spec_Rules' for size function
|
| #
6fc0f068 |
|
28-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "Union", "Inter";
|
| #
26ece69c |
|
05-Nov-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
a301c646 |
|
12-Jul-2015 |
Lars Hupel <lars.hupel@mytum.de> |
Quickcheck setup for finite sets
|
| #
94ea3a82 |
|
06-Jul-2015 |
wenzelm <none@none> |
tuned proofs;
|
| #
a0af5cdd |
|
17-Jun-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
5469d920 |
|
05-Dec-2014 |
kuncar <none@none> |
tuned proof; forget the transfer rule for size_fset
|
| #
34a3534a |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
| #
3816e708 |
|
27-Jun-2014 |
blanchet <none@none> |
merged two small theory files
|
| #
aea2cf85 |
|
23-Apr-2014 |
blanchet <none@none> |
localize new size function generation code
|
| #
fd7ab263 |
|
23-Apr-2014 |
blanchet <none@none> |
added 'size' of finite sets
|
| #
85e48936 |
|
10-Apr-2014 |
kuncar <none@none> |
simplify and fix theories thanks to 356a5efdb278
|
| #
e9e8c934 |
|
10-Apr-2014 |
kuncar <none@none> |
setup for Transfer and Lifting from BNF; tuned thm names
--HG--
rename : src/HOL/Tools/transfer.ML => src/HOL/Tools/Transfer/transfer.ML
|
| #
15939e27 |
|
10-Apr-2014 |
kuncar <none@none> |
abstract Domainp in relator_domain rules => more natural statement of the rule
|
| #
128e121b |
|
10-Apr-2014 |
kuncar <none@none> |
more appropriate name (Lifting.invariant -> eq_onp)
|
| #
845456ae |
|
10-Apr-2014 |
kuncar <none@none> |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
| #
4f5ebd94 |
|
16-Mar-2014 |
haftmann <none@none> |
normalising simp rules for compound operators
|
| #
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
| #
79f2884f |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'sum_rel' to 'rel_sum'
|
| #
da006ee0 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'set_rel' to 'rel_set'
|
| #
8f4cc77e |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fset_rel' to 'rel_fset'
|
| #
59702305 |
|
25-Feb-2014 |
kuncar <none@none> |
simplify a proof due to 6c95a39348bd
|
| #
7c00ce5d |
|
25-Feb-2014 |
kuncar <none@none> |
simplify and repair proofs due to df0fda378813
|
| #
ce5e3fc9 |
|
18-Feb-2014 |
kuncar <none@none> |
simplify proofs because of the stronger reflexivity prover
|
| #
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
| #
325c96bf |
|
24-Jan-2014 |
blanchet <none@none> |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
| #
19339e2f |
|
05-Nov-2013 |
hoelzl <none@none> |
use bdd_above and bdd_below for conditionally complete lattices
|
| #
a32752f9 |
|
01-Oct-2013 |
traytel <none@none> |
base the fset bnf on the new FSet theory
|
| #
8802951a |
|
28-Sep-2013 |
wenzelm <none@none> |
proper document markup;
|
| #
90b3d540 |
|
27-Sep-2013 |
kuncar <none@none> |
tuned names
|
| #
214b43c7 |
|
27-Sep-2013 |
kuncar <none@none> |
fold and lemmas about cardinality
|
| #
3d69ba2c |
|
27-Sep-2013 |
kuncar <none@none> |
new theory of finite sets as a subtype
|