src/Tools/Haskell/Haskell.thy

 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Term (
   Indexname, Sort, Typ(..), Term(..),
   Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs, strip_abs,
-  type_op0, type_op1, op0, op1, op2, typed_op2, binder,
+  type_op0, type_op1, op0, op1, op2, typed_op1, typed_op2, binder,
   dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
   aconv, list_comb, strip_comb, head_of
 )
 where
 

   where
     mk t u = App (App (Const (name, []), t), u)
     dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
     dest _ = Nothing
 
+typed_op1 :: Name -> (Typ -> Term -> Term, Term -> Maybe (Typ, Term))
+typed_op1 name = (mk, dest)
+  where
+    mk ty t = App (Const (name, [ty]), t)
+    dest (App (Const (c, [ty]), t)) | c == name = Just (ty, t)
+    dest _ = Nothing
+
 typed_op2 :: Name -> (Typ -> Term -> Term -> Term, Term -> Maybe (Typ, Term, Term))
 typed_op2 name = (mk, dest)
   where
     mk ty t u = App (App (Const (name, [ty]), t), u)
     dest (App (App (Const (c, [ty]), t), u)) | c == name = Just (ty, t, u)

 -}
 
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Pure (
-  mk_forall, dest_forall, mk_equals, dest_equals, mk_implies, dest_implies
+  mk_forall_op, dest_forall_op, mk_forall, dest_forall,
+  mk_equals, dest_equals, mk_implies, dest_implies
 )
 where
 
 import qualified Isabelle.Name as Name
 import Isabelle.Term
+
+mk_forall_op :: Typ -> Term -> Term; dest_forall_op :: Term -> Maybe (Typ, Term)
+(mk_forall_op, dest_forall_op) = typed_op1 \<open>\<^const_name>\<open>Pure.all\<close>\<close>
 
 mk_forall :: Free -> Term -> Term; dest_forall :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_forall, dest_forall) = binder \<open>\<^const_name>\<open>Pure.all\<close>\<close>
 
 mk_equals :: Typ -> Term -> Term -> Term; dest_equals :: Term -> Maybe (Typ, Term, Term)

   boolT, is_boolT, mk_trueprop, dest_trueprop,
   mk_setT, dest_setT, mk_mem, dest_mem,
   mk_eq, dest_eq, true, is_true, false, is_false,
   mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj,
   mk_imp, dest_imp, mk_iff, dest_iff,
+  mk_all_op, dest_all_op, mk_ex_op, dest_ex_op,
   mk_all, dest_all, mk_ex, dest_ex
 )
 where
 
 import qualified Isabelle.Name as Name

 dest_iff :: Term -> Maybe (Term, Term)
 dest_iff tm =
   case dest_eq tm of
     Just (ty, t, u) | ty == boolT -> Just (t, u)
     _ -> Nothing
+
+mk_all_op :: Typ -> Term -> Term; dest_all_op :: Term -> Maybe (Typ, Term)
+(mk_all_op, dest_all_op) = typed_op1 \<open>\<^const_name>\<open>All\<close>\<close>
+
+mk_ex_op :: Typ -> Term -> Term; dest_ex_op :: Term -> Maybe (Typ, Term)
+(mk_ex_op, dest_ex_op) = typed_op1 \<open>\<^const_name>\<open>Ex\<close>\<close>
 
 mk_all :: Free -> Term -> Term; dest_all :: Name.Context -> Term -> Maybe (Free, Term)
 (mk_all, dest_all) = binder \<open>\<^const_name>\<open>All\<close>\<close>
 
 mk_ex :: Free -> Term -> Term; dest_ex :: Name.Context -> Term -> Maybe (Free, Term)