#
0c4f403a |
|
27-Jan-2020 |
paulson <lp15@cam.ac.uk> |
A few lemmas connected with orderings
|
#
4f45107a |
|
10-Mar-2019 |
haftmann <none@none> |
dropped superfluous declaration attribute --HG-- extra : rebase_source : 9dfb0d90ac0919b01e3567575a0016ebbee2f509
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
ec8d5b30 |
|
10-Nov-2018 |
haftmann <none@none> |
clarified status of legacy input abbreviations
|
#
5128613b |
|
16-Jun-2018 |
nipkow <none@none> |
moved lemmas from AFP
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
c7fc4ed4 |
|
16-Aug-2017 |
nipkow <none@none> |
more reorganization around sorted_wrt
|
#
e736333f |
|
15-Aug-2017 |
nipkow <none@none> |
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
|
#
241de186 |
|
22-Dec-2016 |
haftmann <none@none> |
proper logical constants
|
#
925822fb |
|
21-Dec-2016 |
haftmann <none@none> |
prefer existing logical constant over abbreviation
|
#
218d4808 |
|
21-Dec-2016 |
haftmann <none@none> |
dropped aliasses
|
#
c0bff3d2 |
|
17-Dec-2016 |
haftmann <none@none> |
added lemmas demanded by FIXMEs --HG-- extra : rebase_source : e2ab419767bc144791eca05f3065038591a1bba7
|
#
45a0e905 |
|
05-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
8d2fb663 |
|
28-Jul-2016 |
Andreas Lochbihler <none@none> |
prefer [simp] over [iff] as [iff] break HOL-UNITY
|
#
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;
|
#
b5937653 |
|
04-Jul-2016 |
haftmann <none@none> |
default one-step rules for predicates on relations; clarified status of legacy input abbreviations
|
#
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
#
8b08bf14 |
|
07-Jan-2016 |
paulson <none@none> |
revisions to limits and derivatives, plus new lemmas
|
#
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;
|
#
3487f527 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
#
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
#
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
b4ae9938 |
|
14-Apr-2015 |
Andreas Lochbihler <none@none> |
add lemmas
|
#
f5db77f8 |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
add lemma
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
caa51abc |
|
06-Sep-2014 |
haftmann <none@none> |
added various facts
|
#
1680965a |
|
29-May-2014 |
nipkow <none@none> |
typo
|
#
7812dc7c |
|
29-Apr-2014 |
wenzelm <none@none> |
prefer plain ASCII / latex over not-so-universal Unicode;
|
#
e121e77d |
|
26-Apr-2014 |
haftmann <none@none> |
more complete classical rules for Inf and Sup, modelled after theiry counterparts on Inter and Union (and INF and SUP) --HG-- extra : rebase_source : 710314bbc990dc6cb912a800546a75f7c3a07dca
|
#
d766ca99 |
|
12-Apr-2014 |
haftmann <none@none> |
more operations and lemmas --HG-- extra : rebase_source : 8f5be7e0cdc09c667e66c2cda2c667d4da6e5f73
|
#
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
|
#
3eabe156 |
|
13-Mar-2014 |
blanchet <none@none> |
killed a few 'metis' calls
|
#
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
#
56332e73 |
|
21-Jan-2014 |
traytel <none@none> |
removed theory dependency of BNF_LFP on Datatype
|
#
e3355c3e |
|
20-Jan-2014 |
blanchet <none@none> |
move BNF_LFP up the dependency chain
|
#
304043a6 |
|
29-Nov-2013 |
traytel <none@none> |
set_comprehension_pointfree simproc causes to many surprises if enabled by default
|
#
f55a6e4d |
|
21-Nov-2013 |
blanchet <none@none> |
rationalize imports
|
#
6ba86302 |
|
12-Nov-2013 |
hoelzl <none@none> |
countability of the image of a reflexive transitive closure
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
cd0a3ffe |
|
17-Sep-2013 |
nipkow <none@none> |
added lemmas and made concerse executable
|
#
c199bdb2 |
|
27-Jul-2013 |
traytel <none@none> |
more converse(p) theorems; tuned proofs;
|
#
9862f395 |
|
24-Jul-2013 |
traytel <none@none> |
two useful relation theorems
|
#
1a175983 |
|
19-Jun-2013 |
nipkow <none@none> |
added lemma
|
#
825ed833 |
|
07-Dec-2012 |
nipkow <none@none> |
corrected nonsensical associativity of `` and dvd
|
#
69de248f |
|
31-Jul-2012 |
kuncar <none@none> |
more relation operations expressed by Finite_Set.fold
|
#
c99b1333 |
|
12-Jul-2012 |
bulwahn <none@none> |
a first guess to avoid the Codegenerator_Test to loop infinitely
|
#
7bae30d6 |
|
16-May-2012 |
kuncar <none@none> |
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
|
#
7830ddf3 |
|
05-Apr-2012 |
huffman <none@none> |
define reflp directly, in the manner of symp and transp
|
#
c03a8511 |
|
03-Apr-2012 |
griff <none@none> |
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
|
#
55e11b0d |
|
03-Apr-2012 |
griff <none@none> |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
#
03b58a22 |
|
22-Mar-2012 |
haftmann <none@none> |
fixed typo --HG-- extra : rebase_source : 9faceaa5d14f848f5ee57337e43dc5862026a24d
|
#
24cea092 |
|
17-Mar-2012 |
haftmann <none@none> |
spelt out missing colemmas
|
#
5dbad353 |
|
17-Mar-2012 |
haftmann <none@none> |
generalized INF_INT_eq, SUP_UN_eq
|
#
81c2aa38 |
|
12-Mar-2012 |
noschinl <none@none> |
tuned proofs
|
#
f9beedb8 |
|
12-Mar-2012 |
noschinl <none@none> |
tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
|
#
f9af5d85 |
|
12-Mar-2012 |
noschinl <none@none> |
tuned simpset
|
#
a032bf96 |
|
07-Mar-2012 |
haftmann <none@none> |
tuned syntax; more candidates
|
#
74bda1ac |
|
02-Mar-2012 |
haftmann <none@none> |
more fundamental pred-to-set conversions for range and domain by means of inductive_set --HG-- extra : rebase_source : 62271b2da0fd52b8b598bb504eb41798590b3fa8
|
#
94314ed4 |
|
01-Mar-2012 |
haftmann <none@none> |
more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)
|
#
af2e3acc |
|
26-Feb-2012 |
haftmann <none@none> |
restored accidental omission --HG-- extra : rebase_source : ce6b28d721d05f6bc75668880dc59ca2f21ee33c
|
#
9b9cc610 |
|
26-Feb-2012 |
haftmann <none@none> |
tuned structure --HG-- extra : rebase_source : ceab636a9cfa6e8738a3cb651a7de9e3e87a8911
|
#
5d3088f4 |
|
26-Feb-2012 |
haftmann <none@none> |
tuned structure; dropped already existing syntax declarations --HG-- extra : rebase_source : 3aff5061aebc337202220f0749aab8c247737823
|
#
92c9b3bf |
|
26-Feb-2012 |
haftmann <none@none> |
tuned syntax declarations; tuned structure --HG-- extra : rebase_source : 1b6c21e91abe00bbf0ca93b6c0f5a24da0bef488
|
#
1cc410e1 |
|
26-Feb-2012 |
haftmann <none@none> |
marked candidates for rule declarations
|
#
484c9d58 |
|
24-Feb-2012 |
haftmann <none@none> |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy --HG-- extra : rebase_source : ed15629634477aff0a8efea30547f496c70907ad
|
#
02887bdb |
|
24-Feb-2012 |
haftmann <none@none> |
explicit remove of lattice notation
|
#
37822d49 |
|
23-Feb-2012 |
haftmann <none@none> |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
#
ad4d9474 |
|
30-Jan-2012 |
nipkow <none@none> |
added "'a rel"
|
#
26ada052 |
|
01-Jan-2012 |
haftmann <none@none> |
cleanup of code declarations --HG-- extra : rebase_source : 7376929a640011e27309be6654ccf370df37e60a
|
#
baa19534 |
|
24-Dec-2011 |
haftmann <none@none> |
dropped obsolete code equation for Id
|
#
09ec04b4 |
|
13-Oct-2011 |
haftmann <none@none> |
moved acyclic predicate up in hierarchy --HG-- extra : rebase_source : 4c9a0c3c1dd3de32826493a20016e209648a4e47
|
#
0f6d12b7 |
|
13-Oct-2011 |
haftmann <none@none> |
modernized definitions --HG-- extra : rebase_source : d50ecbd4a46b11ec1f49c3eb54ad2ee86a8981ce
|
#
6971946a |
|
20-Sep-2011 |
haftmann <none@none> |
tuned specification and lemma distribution among theories; tuned proofs
|
#
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
7994d347 |
|
18-Aug-2011 |
haftmann <none@none> |
observe distinction between sets and predicates more properly
|
#
47bb2a89 |
|
21-Feb-2011 |
blanchet <none@none> |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
#
f4cfb277 |
|
07-Dec-2010 |
bulwahn <none@none> |
adding a definition for refl_on which is friendly for quickcheck and nitpick
|
#
0e522e19 |
|
03-Dec-2010 |
bulwahn <none@none> |
adding a nice definition of Id_on for quickcheck and nitpick
|
#
74bcdcc5 |
|
08-May-2010 |
krauss <none@none> |
added lemmas rel_comp_UNION_distrib(2)
|
#
21c81ddb |
|
07-May-2010 |
krauss <none@none> |
removed semicolons
|
#
effccf7c |
|
07-May-2010 |
krauss <none@none> |
rule subrelI (for nice Isar proofs of relation inequalities)
|
#
206a5436 |
|
17-Mar-2010 |
blanchet <none@none> |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
#
ecd3694e |
|
26-Oct-2009 |
krauss <none@none> |
lemma converse_inv_image
|
#
c34b9889 |
|
05-Oct-2009 |
paulson <none@none> |
New facts about domain and range in
|
#
90295cf6 |
|
01-Oct-2009 |
haftmann <none@none> |
proper merge of interpretation equations
|
#
8320083d |
|
31-Aug-2009 |
krauss <none@none> |
moved lemma Wellfounded.in_inv_image to Relation.thy
|
#
263e675f |
|
27-Jul-2009 |
krauss <none@none> |
"more standard" argument order of relation composition (op O)
|
#
dc27ab49 |
|
28-Apr-2009 |
haftmann <none@none> |
ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
bb2d682e |
|
02-Mar-2009 |
nipkow <none@none> |
name changes
|
#
09944fb8 |
|
11-Feb-2009 |
nipkow <none@none> |
Moved Order_Relation into Library and moved some of it into Relation. --HG-- rename : src/HOL/Order_Relation.thy => src/HOL/Library/Order_Relation.thy
|
#
73d9a35c |
|
21-Jan-2009 |
haftmann <none@none> |
changed import hierarchy
|
#
a761f8c1 |
|
26-Aug-2008 |
krauss <none@none> |
added distributivity of relation composition over union [simp]
|
#
70975e92 |
|
17-Mar-2008 |
nipkow <none@none> |
added lemmas
|
#
6cef3e0f |
|
14-Mar-2008 |
nipkow <none@none> |
Added lemmas
|
#
d030298f |
|
08-Oct-2007 |
haftmann <none@none> |
integrated FixedPoint into Inductive
|
#
35ae3509 |
|
14-Aug-2007 |
paulson <none@none> |
ATP blacklisting is now in theory data, attribute noatp
|
#
6a161868 |
|
10-Jul-2007 |
haftmann <none@none> |
moved lfp_induct2 here
|
#
cec07447 |
|
01-Jun-2007 |
krauss <none@none> |
Added simp-rules: "R O {} = {}" and "{} O R = {}"
|
#
c41552bd |
|
24-Jan-2007 |
paulson <none@none> |
some new lemmas
|
#
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
#
cbb1a051 |
|
07-Nov-2006 |
wenzelm <none@none> |
renamed 'const_syntax' to 'notation';
|
#
1e731d3a |
|
26-Sep-2006 |
krauss <none@none> |
Changed precedence of "op O" (relation composition) from 60 to 75.
|
#
61bd82ad |
|
16-May-2006 |
wenzelm <none@none> |
tuned concrete syntax -- abbreviation/const_syntax;
|
#
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.
|
#
ca6e4a30 |
|
09-Mar-2006 |
huffman <none@none> |
added many simple lemmas
|
#
0789ab36 |
|
22-Sep-2005 |
nipkow <none@none> |
renamed rules to iprover
|
#
50a9ed6e |
|
03-Sep-2004 |
paulson <none@none> |
new theorem symD
|
#
0fe1d442 |
|
18-Aug-2004 |
nipkow <none@none> |
import -> imports
|
#
e61c8d7d |
|
16-Aug-2004 |
nipkow <none@none> |
New theory header syntax.
|
#
61c8b93b |
|
26-Feb-2003 |
paulson <none@none> |
some x-symbols and some new lemmas
|
#
5bb51f23 |
|
08-Feb-2003 |
paulson <none@none> |
converting HOL/UNITY to use unconditional fairness
|
#
1f2549c2 |
|
10-Oct-2002 |
berghofe <none@none> |
Removed obsolete function "fun_rel_comp".
|
#
084e5d05 |
|
30-Aug-2002 |
paulson <none@none> |
removal of blast.overloaded
|
#
854e6b5a |
|
11-Jul-2002 |
nipkow <none@none> |
*** empty log message ***
|
#
cf2fff3e |
|
21-Feb-2002 |
wenzelm <none@none> |
fixed document; tuned;
|
#
b1794309 |
|
20-Feb-2002 |
berghofe <none@none> |
Converted to new theory format.
|
#
ca7ddbd5 |
|
13-Dec-2001 |
nipkow <none@none> |
comp -> rel_comp
|
#
b6fd44a8 |
|
15-Feb-2001 |
oheimb <none@none> |
moved inv_image to Relation
|
#
ee7fa931 |
|
09-Jan-2001 |
nipkow <none@none> |
`` -> and ``` -> ``
|
#
2c1f2b82 |
|
05-Jan-2001 |
nipkow <none@none> |
^^ -> ``` Univalent -> single_valued
|
#
a8f3b6fa |
|
05-Jan-2001 |
paulson <none@none> |
Field of a relation, and some Domain/Range rules
|
#
bc3e357c |
|
30-Oct-2000 |
wenzelm <none@none> |
converse: syntax \<inverse>;
|
#
bc286955 |
|
12-Oct-2000 |
nipkow <none@none> |
*** empty log message ***
|
#
dc3bc48c |
|
13-Apr-2000 |
nipkow <none@none> |
Times -> <*> ** -> <*lex*>
|
#
667c4527 |
|
21-Feb-2000 |
oheimb <none@none> |
renamed Univalent to univalent
|
#
a451263a |
|
22-Oct-1999 |
paulson <none@none> |
tidied using modern infix form
|
#
af8dff48 |
|
15-Jul-1999 |
berghofe <none@none> |
Added some definitions and theorems needed for the construction of datatypes involving function types.
|
#
421a0321 |
|
10-Jun-1999 |
paulson <none@none> |
new preficates refl, sym [from Integ/Equiv], antisym
|
#
b83ef86b |
|
27-Nov-1998 |
paulson <none@none> |
moved diag (diagonal relation) from Univ to Relation
|
#
5ef6afb1 |
|
02-Oct-1998 |
nipkow <none@none> |
id <-> Id
|
#
6d8d84fb |
|
16-Mar-1998 |
paulson <none@none> |
inverse -> converse [It is standard terminology and also used in ZF]
|
#
0bb3291a |
|
08-Jan-1998 |
oheimb <none@none> |
added Univalent
|
#
80eec34e |
|
04-Jul-1997 |
nipkow <none@none> |
Reduced priority of postfix ^* etc operators such that they are the same as application. Eg wf r^* now needs to be written wf(r^*).
|
#
952ce112 |
|
17-Jun-1997 |
nipkow <none@none> |
converse -> ^-1
|
#
7720da9b |
|
12-Sep-1996 |
paulson <none@none> |
Simplification and tidying of definitions
|
#
606e723f |
|
26-Apr-1996 |
nipkow <none@none> |
Generalized types of some of the operators (thanks to Norbert Voelker)
|
#
1d43e2fa |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
|
#
9c75800b |
|
26-Jan-1996 |
nipkow <none@none> |
Streamlined defs in Relation and added new intro/elim rules to do with pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...
|
#
c8adb285 |
|
26-May-1995 |
nipkow <none@none> |
Trancl is now based on Relation which used to be in Integ.
|