src/HOL/Relation.thy
changeset 56742 678a52e676b6
parent 56545 8f1e7596deb7
child 56790 f54097170704
     1.1 --- a/src/HOL/Relation.thy	Sat Apr 26 13:25:46 2014 +0200
     1.2 +++ b/src/HOL/Relation.thy	Sat Apr 26 14:53:22 2014 +0200
     1.3 @@ -30,15 +30,25 @@
     1.4  declare sup2E [elim!]
     1.5  declare sup1CI [intro!]
     1.6  declare sup2CI [intro!]
     1.7 +declare Inf1_I [intro!]
     1.8  declare INF1_I [intro!]
     1.9 +declare Inf2_I [intro!]
    1.10  declare INF2_I [intro!]
    1.11 +declare Inf1_D [elim]
    1.12  declare INF1_D [elim]
    1.13 +declare Inf2_D [elim]
    1.14  declare INF2_D [elim]
    1.15 +declare Inf1_E [elim]
    1.16  declare INF1_E [elim]
    1.17 +declare Inf2_E [elim]
    1.18  declare INF2_E [elim]
    1.19 +declare Sup1_I [intro]
    1.20  declare SUP1_I [intro]
    1.21 +declare Sup2_I [intro]
    1.22  declare SUP2_I [intro]
    1.23 +declare Sup1_E [elim!]
    1.24  declare SUP1_E [elim!]
    1.25 +declare Sup2_E [elim!]
    1.26  declare SUP2_E [elim!]
    1.27  
    1.28  subsection {* Fundamental *}