21   val dest_fsetT: typ -> typ

    21   val dest_fsetT: typ -> typ

    22 

    22 

    23   val mk_id: term -> term

    23   val mk_id: term -> term

    24   val mk_all: (string * typ) -> term -> term

    24   val mk_all: (string * typ) -> term -> term

    25   val mk_All: (string * typ) -> term -> term

    25   val mk_All: (string * typ) -> term -> term

    26 

    27 

    27   val sum_case_const: typ -> typ -> typ -> term

    28   val sum_case_const: typ -> typ -> typ -> term

    28   val mk_sum_case: term -> term -> term

    29   val mk_sum_case: term -> term -> term

    29  

    30  

    30   val mk_minus: term -> term

    31   val mk_minus: term -> term

   201 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm

   202 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm

   202 

   203 

   203 fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)

   204 fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)

   204 

   205 

   205 fun mk_All (a, T) t =  HOLogic.all_const T $ Abs (a, T, t)

   206 fun mk_All (a, T) t =  HOLogic.all_const T $ Abs (a, T, t)

   206 

   209 

   207 fun sum_case_const ty1 ty2 ty3 = 

   210 fun sum_case_const ty1 ty2 ty3 = 

   208   Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)

   211   Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)

   209 

   212 

   210 fun mk_sum_case trm1 trm2 =

   213 fun mk_sum_case trm1 trm2 =