src/FOL/fologic.ML
changeset 69593 3dda49e08b9d
parent 44241 7943b69f0188
     1.1 --- a/src/FOL/fologic.ML	Fri Jan 04 21:49:06 2019 +0100
     1.2 +++ b/src/FOL/fologic.ML	Fri Jan 04 23:22:53 2019 +0100
     1.3 @@ -37,48 +37,48 @@
     1.4  structure FOLogic: FOLOGIC =
     1.5  struct
     1.6  
     1.7 -val oT = Type(@{type_name o},[]);
     1.8 +val oT = Type(\<^type_name>\<open>o\<close>,[]);
     1.9  
    1.10 -val Trueprop = Const(@{const_name Trueprop}, oT-->propT);
    1.11 +val Trueprop = Const(\<^const_name>\<open>Trueprop\<close>, oT-->propT);
    1.12  
    1.13  fun mk_Trueprop P = Trueprop $ P;
    1.14  
    1.15 -fun dest_Trueprop (Const (@{const_name Trueprop}, _) $ P) = P
    1.16 +fun dest_Trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ P) = P
    1.17    | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    1.18  
    1.19  
    1.20  (* Logical constants *)
    1.21  
    1.22 -val not = Const (@{const_name Not}, oT --> oT);
    1.23 -val conj = Const(@{const_name conj}, [oT,oT]--->oT);
    1.24 -val disj = Const(@{const_name disj}, [oT,oT]--->oT);
    1.25 -val imp = Const(@{const_name imp}, [oT,oT]--->oT)
    1.26 -val iff = Const(@{const_name iff}, [oT,oT]--->oT);
    1.27 +val not = Const (\<^const_name>\<open>Not\<close>, oT --> oT);
    1.28 +val conj = Const(\<^const_name>\<open>conj\<close>, [oT,oT]--->oT);
    1.29 +val disj = Const(\<^const_name>\<open>disj\<close>, [oT,oT]--->oT);
    1.30 +val imp = Const(\<^const_name>\<open>imp\<close>, [oT,oT]--->oT)
    1.31 +val iff = Const(\<^const_name>\<open>iff\<close>, [oT,oT]--->oT);
    1.32  
    1.33  fun mk_conj (t1, t2) = conj $ t1 $ t2
    1.34  and mk_disj (t1, t2) = disj $ t1 $ t2
    1.35  and mk_imp (t1, t2) = imp $ t1 $ t2
    1.36  and mk_iff (t1, t2) = iff $ t1 $ t2;
    1.37  
    1.38 -fun dest_imp (Const(@{const_name imp},_) $ A $ B) = (A, B)
    1.39 +fun dest_imp (Const(\<^const_name>\<open>imp\<close>,_) $ A $ B) = (A, B)
    1.40    | dest_imp  t = raise TERM ("dest_imp", [t]);
    1.41  
    1.42 -fun dest_conj (Const (@{const_name conj}, _) $ t $ t') = t :: dest_conj t'
    1.43 +fun dest_conj (Const (\<^const_name>\<open>conj\<close>, _) $ t $ t') = t :: dest_conj t'
    1.44    | dest_conj t = [t];
    1.45  
    1.46 -fun dest_iff (Const(@{const_name iff},_) $ A $ B) = (A, B)
    1.47 +fun dest_iff (Const(\<^const_name>\<open>iff\<close>,_) $ A $ B) = (A, B)
    1.48    | dest_iff  t = raise TERM ("dest_iff", [t]);
    1.49  
    1.50 -fun eq_const T = Const (@{const_name eq}, [T, T] ---> oT);
    1.51 +fun eq_const T = Const (\<^const_name>\<open>eq\<close>, [T, T] ---> oT);
    1.52  fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
    1.53  
    1.54 -fun dest_eq (Const (@{const_name eq}, _) $ lhs $ rhs) = (lhs, rhs)
    1.55 +fun dest_eq (Const (\<^const_name>\<open>eq\<close>, _) $ lhs $ rhs) = (lhs, rhs)
    1.56    | dest_eq t = raise TERM ("dest_eq", [t])
    1.57  
    1.58 -fun all_const T = Const (@{const_name All}, [T --> oT] ---> oT);
    1.59 +fun all_const T = Const (\<^const_name>\<open>All\<close>, [T --> oT] ---> oT);
    1.60  fun mk_all (Free (x, T), P) = all_const T $ absfree (x, T) P;
    1.61  
    1.62 -fun exists_const T = Const (@{const_name Ex}, [T --> oT] ---> oT);
    1.63 +fun exists_const T = Const (\<^const_name>\<open>Ex\<close>, [T --> oT] ---> oT);
    1.64  fun mk_exists (Free (x, T), P) = exists_const T $ absfree (x, T) P;
    1.65  
    1.66