src/FOL/fologic.ML
changeset 44241 7943b69f0188
parent 41310 65631ca437c9
child 69593 3dda49e08b9d
equal deleted inserted replaced
44240:4b1a63678839 44241:7943b69f0188
    74 
    74 
    75 fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
    75 fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
    76   | dest_eq t = raise TERM ("dest_eq", [t])
    76   | dest_eq t = raise TERM ("dest_eq", [t])
    77 
    77 
    78 fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
    78 fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
    79 fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
    79 fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
    80 
    80 
    81 fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
    81 fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
    82 fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
    82 fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
    83 
    83 
    84 
    84 
    85 (* binary oprations and relations *)
    85 (* binary oprations and relations *)
    86 
    86 
    87 fun mk_binop c (t, u) =
    87 fun mk_binop c (t, u) =