--- a/src/HOL/Fun.thy Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Fun.thy Mon Jun 23 23:45:39 2008 +0200
@@ -509,7 +509,7 @@
case find_double t of
(T, NONE) => NONE
| (T, SOME rhs) =>
- SOME (Goal.prove ctxt [] [] (Term.equals T $ t $ rhs)
+ SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
(fn _ =>
rtac eq_reflection 1 THEN
rtac ext 1 THEN
--- a/src/HOL/Hoare/HoareAbort.thy Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy Mon Jun 23 23:45:39 2008 +0200
@@ -305,8 +305,7 @@
(Free ("P",varsT --> boolT) $ mk_bodyC vars));
val small_Collect = mk_CollectC (Abs("x",varsT,
Free ("P",varsT --> boolT) $ Bound 0));
- val impl = implies $ (Mset_incl big_Collect) $
- (Mset_incl small_Collect);
+ val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
end;
--- a/src/HOL/Hoare/hoare_tac.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Mon Jun 23 23:45:39 2008 +0200
@@ -72,8 +72,7 @@
(Free ("P",varsT --> boolT) $ mk_bodyC vars));
val small_Collect = mk_CollectC (Abs("x",varsT,
Free ("P",varsT --> boolT) $ Bound 0));
- val impl = implies $ (Mset_incl big_Collect) $
- (Mset_incl small_Collect);
+ val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
end;
--- a/src/HOL/Import/shuffler.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Import/shuffler.ML Mon Jun 23 23:45:39 2008 +0200
@@ -159,13 +159,15 @@
val cert = cterm_of Pure.thy
val xT = TFree("'a",[])
val yT = TFree("'b",[])
+ val x = Free("x",xT)
+ val y = Free("y",yT)
val P = Free("P",xT-->yT-->propT)
- val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
- val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
+ val lhs = Logic.all x (Logic.all y (P $ x $ y))
+ val rhs = Logic.all y (Logic.all x (P $ x $ y))
val cl = cert lhs
val cr = cert rhs
- val cx = cert (Free("x",xT))
- val cy = cert (Free("y",yT))
+ val cx = cert x
+ val cy = cert y
val th1 = assume cr
|> forall_elim_list [cy,cx]
|> forall_intr_list [cx,cy]
@@ -415,6 +417,8 @@
fun mk_free s t = Free (s,t)
val xT = mk_tfree "a"
val yT = mk_tfree "b"
+val x = Free ("x", xT)
+val y = Free ("y", yT)
val P = mk_free "P" (xT-->yT-->propT)
val Q = mk_free "Q" (xT-->yT)
val R = mk_free "R" (xT-->yT)
@@ -436,7 +440,7 @@
fun quant_simproc thy = Simplifier.simproc_i
thy
"Ordered rewriting of nested quantifiers"
- [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
+ [Logic.all x (Logic.all y (P $ x $ y))]
quant_rewrite
fun eta_expand_simproc thy = Simplifier.simproc_i
thy
@@ -446,7 +450,7 @@
fun eta_contract_simproc thy = Simplifier.simproc_i
thy
"Smart handling of eta-contractions"
- [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
+ [Logic.all x (Logic.mk_equals (Q $ x, R $ x))]
eta_contract
end
@@ -582,8 +586,7 @@
fun set_prop thy t =
let
val vars = add_term_frees (t,add_term_vars (t,[]))
- val closed_t = Library.foldr (fn (v, body) =>
- let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
+ val closed_t = fold_rev Logic.all vars t
val rew_th = norm_term thy closed_t
val rhs = Thm.rhs_of rew_th
--- a/src/HOL/Statespace/state_fun.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Statespace/state_fun.ML Mon Jun 23 23:45:39 2008 +0200
@@ -251,7 +251,7 @@
(trm,trm',vars,_,true)
=> let
val eq1 = Goal.prove ctxt [] []
- (list_all (vars,equals sT$trm$trm'))
+ (list_all (vars, Logic.mk_equals (trm, trm')))
(fn _ => rtac meta_ext 1 THEN
simp_tac ss1 1);
val eq2 = Simplifier.asm_full_rewrite ss2 (Thm.dest_equals_rhs (cprop_of eq1));
--- a/src/HOL/Tools/Qelim/cooper.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon Jun 23 23:45:39 2008 +0200
@@ -637,8 +637,8 @@
let
val (vs, ps) = pairself (map_index swap) (term_frees t, term_bools [] t);
in
- equals propT $ HOLogic.mk_Trueprop t $
- HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t)))
+ Logic.mk_equals (HOLogic.mk_Trueprop t,
+ HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
end;
end;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Jun 23 23:45:39 2008 +0200
@@ -237,8 +237,8 @@
val rep_name = Sign.intern_const thy ("Rep_" ^ tname);
val lhs = list_comb (Const (cname, constrT), l_args);
val rhs = mk_univ_inj r_args n i;
- val def = equals T $ lhs $ (Const (abs_name, Univ_elT --> T) $ rhs);
- val def_name = (Sign.base_name cname) ^ "_def";
+ val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
+ val def_name = Sign.base_name cname ^ "_def";
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
(Const (rep_name, T --> Univ_elT) $ lhs, rhs));
val ([def_thm], thy') =
@@ -346,8 +346,8 @@
val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
val fTs = map fastype_of fs;
val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
- equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
- list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
+ Logic.mk_equals (Const (iso_name, T --> Univ_elT),
+ list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
val (def_thms, thy') = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy;
(* prove characteristic equations *)
--- a/src/HOL/Tools/function_package/context_tree.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML Mon Jun 23 23:45:39 2008 +0200
@@ -177,7 +177,7 @@
fun export_term (fixes, assumes) =
fold_rev (curry Logic.mk_implies o prop_of) assumes
- #> fold_rev (mk_forall o Free) fixes
+ #> fold_rev (Logic.all o Free) fixes
fun export_thm thy (fixes, assumes) =
fold_rev (implies_intr o cprop_of) assumes
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Mon Jun 23 23:45:39 2008 +0200
@@ -152,7 +152,7 @@
fun mk_assum qs pats =
HOLogic.mk_Trueprop P
|> fold_rev (curry Logic.mk_implies o HOLogic.mk_Trueprop o HOLogic.mk_eq) (xs ~~ pats)
- |> fold_rev mk_forall qs
+ |> fold_rev Logic.all qs
|> cterm_of thy
val hyps = map2 mk_assum qss patss
@@ -221,7 +221,7 @@
HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
Const ("HOL.undefined", rT))
|> HOLogic.mk_Trueprop
- |> fold_rev mk_forall qs
+ |> fold_rev Logic.all qs
end
in
map mk_eqn fixes
--- a/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_lib.ML Mon Jun 23 23:45:39 2008 +0200
@@ -21,9 +21,6 @@
fun plural sg pl [x] = sg
| plural sg pl _ = pl
-(* ==> logic.ML? *)
-fun mk_forall v t = all (fastype_of v) $ lambda v t
-
(* lambda-abstracts over an arbitrarily nested tuple
==> hologic.ML? *)
fun tupled_lambda vars t =
@@ -117,7 +114,7 @@
| rename_bound n _ = raise Match
fun mk_forall_rename (n, v) =
- rename_bound n o mk_forall v
+ rename_bound n o Logic.all v
val dummy_term = Free ("", dummyT)
--- a/src/HOL/Tools/function_package/induction_scheme.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/induction_scheme.ML Mon Jun 23 23:45:39 2008 +0200
@@ -146,7 +146,7 @@
HOLogic.mk_Trueprop Pbool
|> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases
|> fold_rev (curry Logic.mk_implies) Cs'
- |> fold_rev (mk_forall o Free) ws
+ |> fold_rev (Logic.all o Free) ws
|> fold_rev mk_forall_rename (map fst xs ~~ xs')
|> mk_forall_rename ("P", Pbool)
end
@@ -169,7 +169,7 @@
val cse =
HOLogic.mk_Trueprop thesis
|> fold_rev (curry Logic.mk_implies) Cs'
- |> fold_rev (mk_forall o Free) ws
+ |> fold_rev (Logic.all o Free) ws
in
Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis)
end
@@ -180,7 +180,7 @@
let val export =
fold_rev (curry Logic.mk_implies) Gas
#> fold_rev (curry Logic.mk_implies) gs
- #> fold_rev (mk_forall o Free) Gvs
+ #> fold_rev (Logic.all o Free) Gvs
#> fold_rev mk_forall_rename (oqnames ~~ map Free qs)
in
(HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R)
@@ -188,7 +188,7 @@
|> export,
mk_pres bidx' rcarg
|> export
- |> mk_forall thesis)
+ |> Logic.all thesis)
end
in
map g rs
@@ -205,7 +205,7 @@
fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
HOLogic.mk_Trueprop (list_comb (P, map Free xs))
|> fold_rev (curry Logic.mk_implies) Cs
- |> fold_rev (mk_forall o Free) ws
+ |> fold_rev (Logic.all o Free) ws
|> term_conv thy ind_atomize
|> ObjectLogic.drop_judgment thy
|> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
@@ -230,13 +230,13 @@
val P_comp = mk_ind_goal thy branches
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
- val ihyp = all T $ Abs ("z", T,
- implies $
- HOLogic.mk_Trueprop (
+ val ihyp = Term.all T $ Abs ("z", T,
+ Logic.mk_implies
+ (HOLogic.mk_Trueprop (
Const ("op :", HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT)
$ (HOLogic.pair_const T T $ Bound 0 $ x)
- $ R)
- $ HOLogic.mk_Trueprop (P_comp $ Bound 0))
+ $ R),
+ HOLogic.mk_Trueprop (P_comp $ Bound 0)))
|> cert
val aihyp = assume ihyp
@@ -290,7 +290,7 @@
val step = HOLogic.mk_Trueprop (list_comb (P, lhs))
|> fold_rev (curry Logic.mk_implies o prop_of) P_recs
|> fold_rev (curry Logic.mk_implies) gs
- |> fold_rev (mk_forall o Free) qs
+ |> fold_rev (Logic.all o Free) qs
|> cert
val Plhs_to_Pxs_conv =
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Mon Jun 23 23:45:39 2008 +0200
@@ -70,8 +70,7 @@
let
val concl = HOLogic.mk_binrel rel (lhs, rhs) |> HOLogic.mk_Trueprop
in
- Logic.list_implies (prems, concl)
- |> fold_rev FundefLib.mk_forall vars
+ fold_rev Logic.all vars (Logic.list_implies (prems, concl))
end
fun prove thy solve_tac t =
--- a/src/HOL/Tools/function_package/pattern_split.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/function_package/pattern_split.ML Mon Jun 23 23:45:39 2008 +0200
@@ -101,7 +101,7 @@
let
val t = Pattern.rewrite_term thy sigma [] feq1
in
- fold_rev mk_forall (map Free (frees_in_term ctx t) inter vs') t
+ fold_rev Logic.all (map Free (frees_in_term ctx t) inter vs') t
end
in
map instantiate substs
--- a/src/HOL/Tools/inductive_realizer.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Mon Jun 23 23:45:39 2008 +0200
@@ -29,14 +29,10 @@
val thm' = Reconstruct.reconstruct_proof thy (Thm.prop_of thm) (Thm.proof_of thm);
in Reconstruct.expand_proof thy [("", NONE)] thm' end; (* FIXME *)
-fun forall_intr_prf (t, prf) =
+fun forall_intr_prf t prf =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
in Abst (a, SOME T, Proofterm.prf_abstract_over t prf) end;
-fun forall_intr_term (t, u) =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in all T $ Abs (a, T, abstract_over (t, u)) end;
-
fun subsets [] = [[]]
| subsets (x::xs) =
let val ys = subsets xs
@@ -264,13 +260,13 @@
val rlzvs = rev (Term.add_vars (prop_of rrule) []);
val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
- val rlz' = foldr forall_intr_term (prop_of rrule) (vs2 @ rs);
- val rlz'' = foldr forall_intr_term rlz vs2
+ val rlz' = fold_rev Logic.all (vs2 @ rs) (prop_of rrule);
+ val rlz'' = fold_rev Logic.all vs2 rlz
in (name, (vs,
if rt = Extraction.nullt then rt else
foldr (uncurry lambda) rt vs1,
ProofRewriteRules.un_hhf_proof rlz' rlz''
- (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
+ (fold_rev forall_intr_prf (vs2 @ rs) (prf_of rrule))))
end;
fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
@@ -427,7 +423,7 @@
let
val (prem :: prems) = prems_of elim;
fun reorder1 (p, (_, intr)) =
- Library.foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t)
+ Library.foldl (fn (t, ((s, _), T)) => Logic.all (Free (s, T)) t)
(strip_all p, Term.add_vars (prop_of intr) [] \\ params');
fun reorder2 ((ivs, intr), i) =
let val fs = Term.add_vars (prop_of intr) [] \\ params'
--- a/src/HOL/Tools/inductive_set_package.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/inductive_set_package.ML Mon Jun 23 23:45:39 2008 +0200
@@ -69,7 +69,7 @@
fun close p t f =
let val vs = Term.add_vars t []
in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
- (p (fold (fn x as (_, T) => fn u => all T $ lambda (Var x) u) vs t) f)
+ (p (fold (Logic.all o Var) vs t) f)
end;
fun mkop "op &" T x = SOME (Const ("op Int", T --> T --> T), x)
| mkop "op |" T x = SOME (Const ("op Un", T --> T --> T), x)
--- a/src/HOL/Tools/record_package.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/record_package.ML Mon Jun 23 23:45:39 2008 +0200
@@ -1050,7 +1050,7 @@
(case mk_eq_terms (upd$k$r) of
SOME (trm,trm',vars)
=> SOME (prove_split_simp thy ss domS
- (list_all(vars,(equals rangeS$(sel$trm)$trm'))))
+ (list_all(vars, Logic.mk_equals (sel $ trm, trm'))))
| NONE => NONE)
end
| NONE => NONE)
@@ -1187,7 +1187,7 @@
Inter (trm,trm',vars,_,_)
=> SOME (normalize_rhs
(prove_split_simp thy ss rT
- (list_all(vars,(equals rT$trm$trm')))))
+ (list_all(vars, Logic.mk_equals (trm, trm')))))
| _ => NONE)
end
| _ => NONE))
--- a/src/HOL/Tools/res_axioms.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML Mon Jun 23 23:45:39 2008 +0200
@@ -86,7 +86,7 @@
(*Forms a lambda-abstraction over the formal parameters*)
val (c, thy') = Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy
val cdef = cname ^ "_def"
- val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy'
+ val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
| dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
@@ -113,7 +113,7 @@
val rhs = list_abs_free (map dest_Free args,
HOLogic.choice_const T $ xtp)
(*Forms a lambda-abstraction over the formal parameters*)
- val def = equals cT $ c $ rhs
+ val def = Logic.mk_equals (c, rhs)
in dec_sko (subst_bound (list_comb(c,args), p))
(def :: defs)
end
--- a/src/HOL/Tools/res_reconstruct.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Mon Jun 23 23:45:39 2008 +0200
@@ -250,12 +250,7 @@
singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt))
end;
-(*Quantification over a list of Vars. FIXME: for term.ML??*)
-fun list_all_var ([], t: term) = t
- | list_all_var ((v as Var(ix,T)) :: vars, t) =
- (all T) $ Abs(string_of_indexname ix, T, abstract_over (v, list_all_var (vars,t)));
-
-fun gen_all_vars t = list_all_var (term_vars t, t);
+fun gen_all_vars t = fold_rev Logic.all (term_vars t) t;
fun ints_of_stree_aux (Int n, ns) = n::ns
| ints_of_stree_aux (Br(_,ts), ns) = foldl ints_of_stree_aux ns ts;
--- a/src/Pure/Proof/extraction.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/Pure/Proof/extraction.ML Mon Jun 23 23:45:39 2008 +0200
@@ -128,10 +128,6 @@
fun vars_of t = rev (fold_aterms (fn v as Var _ => insert (op =) v | _ => I) t []);
fun vfs_of t = vars_of t @ sort Term.term_ord (term_frees t);
-fun forall_intr (t, prop) =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in all T $ Abs (a, T, abstract_over (t, prop)) end;
-
fun forall_intr_prf (t, prf) =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
in Abst (a, SOME T, prf_abstract_over t prf) end;
@@ -324,7 +320,7 @@
(procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
(Const ("realizes", T --> propT --> propT) $
(if T = nullT then t else list_comb (t, vars')) $ prop);
- val r = List.foldr forall_intr r' (map (get_var_type r') vars);
+ val r = fold_rev Logic.all (map (get_var_type r') vars) r';
val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
in (name, (vs, (t, prf))) end
end;
--- a/src/Pure/Proof/reconstruct.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/Pure/Proof/reconstruct.ML Mon Jun 23 23:45:39 2008 +0200
@@ -26,11 +26,7 @@
fun vars_of t = rev (fold_aterms
(fn v as Var _ => insert (op =) v | _ => I) t []);
-fun forall_intr t prop =
- let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
- in all T $ Abs (a, T, abstract_over (t, prop)) end;
-
-fun forall_intr_vfs prop = fold_rev forall_intr
+fun forall_intr_vfs prop = fold_rev Logic.all
(vars_of prop @ sort Term.term_ord (term_frees prop)) prop;
fun forall_intr_prf t prf =
@@ -317,7 +313,7 @@
fun prop_of0 Hs (PBound i) = List.nth (Hs, i)
| prop_of0 Hs (Abst (s, SOME T, prf)) =
- all T $ (Abs (s, T, prop_of0 Hs prf))
+ Term.all T $ (Abs (s, T, prop_of0 Hs prf))
| prop_of0 Hs (AbsP (s, SOME t, prf)) =
Logic.mk_implies (t, prop_of0 (t :: Hs) prf)
| prop_of0 Hs (prf % SOME t) = (case head_norm (prop_of0 Hs prf) of
--- a/src/Pure/proofterm.ML Mon Jun 23 20:00:58 2008 +0200
+++ b/src/Pure/proofterm.ML Mon Jun 23 23:45:39 2008 +0200
@@ -774,13 +774,10 @@
("transitive", list_implies ([mk_equals (x, y), mk_equals (y, z)], mk_equals (x, z))),
("equal_intr", list_implies ([mk_implies (A, B), mk_implies (B, A)], mk_equals (A, B))),
("equal_elim", list_implies ([mk_equals (A, B), A], B)),
- ("abstract_rule", Logic.mk_implies
- (all aT $ Abs ("x", aT, equals bT $ (f $ Bound 0) $ (g $ Bound 0)),
- equals (aT --> bT) $
- Abs ("x", aT, f $ Bound 0) $ Abs ("x", aT, g $ Bound 0))),
- ("combination", Logic.list_implies
- ([Logic.mk_equals (f, g), Logic.mk_equals (x, y)],
- Logic.mk_equals (f $ x, g $ y)))];
+ ("abstract_rule", mk_implies
+ (all x (mk_equals (f $ x, g $ x)), mk_equals (lambda x (f $ x), lambda x (g $ x)))),
+ ("combination", list_implies
+ ([mk_equals (f, g), mk_equals (x, y)], mk_equals (f $ x, g $ y)))];
val [reflexive_axm, symmetric_axm, transitive_axm, equal_intr_axm,
equal_elim_axm, abstract_rule_axm, combination_axm] =