--- a/src/HOL/Tools/BNF/bnf_util.ML Mon Jul 07 16:06:46 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Jul 07 16:06:46 2014 +0200
@@ -123,6 +123,8 @@
val mk_ordLeq_csum: int -> int -> thm -> thm
val mk_UnIN: int -> int -> thm
+ val eqTrueI: thm
+ val eqFalseI: thm
val prod_injectD: thm
val prod_injectI: thm
val ctrans: thm
@@ -518,6 +520,8 @@
fun mk_sym thm = thm RS sym;
(*TODO: antiquote heavily used theorems once*)
+val eqTrueI = @{thm iffD2[OF eq_True]};
+val eqFalseI = @{thm iffD2[OF eq_False]};
val prod_injectD = @{thm iffD1[OF prod.inject]};
val prod_injectI = @{thm iffD2[OF prod.inject]};
val ctrans = @{thm ordLeq_transitive};