--- a/src/HOL/Tools/BNF/bnf_lfp_util.ML Thu Mar 20 23:38:34 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_util.ML Fri Mar 21 08:13:23 2014 +0100
@@ -12,7 +12,6 @@
val mk_bij_betw: term -> term -> term -> term
val mk_cardSuc: term -> term
- val mk_inver: term -> term -> term -> term
val mk_not_empty: term -> term
val mk_not_eq: term -> term -> term
val mk_rapp: term -> typ -> term
@@ -52,10 +51,6 @@
Const (@{const_name bij_betw},
fastype_of f --> fastype_of A --> fastype_of B --> HOLogic.boolT) $ f $ A $ B;
-fun mk_inver f g A =
- Const (@{const_name inver}, fastype_of f --> fastype_of g --> fastype_of A --> HOLogic.boolT) $
- f $ g $ A;
-
fun mk_not_eq x y = HOLogic.mk_not (HOLogic.mk_eq (x, y));
fun mk_not_empty B = mk_not_eq B (HOLogic.mk_set (HOLogic.dest_setT (fastype_of B)) []);