--- a/src/HOL/Relation.thy Sat Apr 26 13:25:46 2014 +0200
+++ b/src/HOL/Relation.thy Sat Apr 26 14:53:22 2014 +0200
@@ -30,15 +30,25 @@
declare sup2E [elim!]
declare sup1CI [intro!]
declare sup2CI [intro!]
+declare Inf1_I [intro!]
declare INF1_I [intro!]
+declare Inf2_I [intro!]
declare INF2_I [intro!]
+declare Inf1_D [elim]
declare INF1_D [elim]
+declare Inf2_D [elim]
declare INF2_D [elim]
+declare Inf1_E [elim]
declare INF1_E [elim]
+declare Inf2_E [elim]
declare INF2_E [elim]
+declare Sup1_I [intro]
declare SUP1_I [intro]
+declare Sup2_I [intro]
declare SUP2_I [intro]
+declare Sup1_E [elim!]
declare SUP1_E [elim!]
+declare Sup2_E [elim!]
declare SUP2_E [elim!]
subsection {* Fundamental *}