src/HOL/BNF/Tools/bnf_gfp_util.ML
changeset 50058 bb1fadeba35e
parent 49510 ba50d204095e
child 51447 a19e973fa2cf
--- a/src/HOL/BNF/Tools/bnf_gfp_util.ML	Tue Nov 13 09:08:32 2012 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_util.ML	Tue Nov 13 12:06:43 2012 +0100
@@ -25,6 +25,7 @@
   val mk_nat_rec: term -> term -> term
   val mk_pickWP: term -> term -> term -> term -> term -> term
   val mk_prefCl: term -> term
+  val mk_prefixeq: term -> term -> term
   val mk_proj: term -> term
   val mk_quotient: term -> term -> term
   val mk_shift: term -> term -> term
@@ -93,6 +94,9 @@
 fun mk_prefCl A =
   Const (@{const_name prefCl}, fastype_of A --> HOLogic.boolT) $ A;
 
+fun mk_prefixeq xs ys =
+  Const (@{const_name prefixeq}, fastype_of xs --> fastype_of ys --> HOLogic.boolT) $ xs $ ys;
+
 fun mk_clists r =
   let val T = fastype_of r;
   in Const (@{const_name clists}, T --> mk_relT (`I (HOLogic.listT (fst (dest_relT T))))) $ r end;