# HG changeset patch # User wenzelm # Date 960316303 -7200 # Node ID 20ff649a0fd1858801d08985da156723ef0079cc # Parent 63d20536971f2a9b916784c2e6f41a7295acbe4d added rule_params; diff -r 63d20536971f -r 20ff649a0fd1 src/Provers/split_paired_all.ML --- a/src/Provers/split_paired_all.ML Tue Jun 06 20:31:22 2000 +0200 +++ b/src/Provers/split_paired_all.ML Tue Jun 06 20:31:43 2000 +0200 @@ -12,6 +12,7 @@ signature SPLIT_PAIRED_ALL = sig + val rule_params: string -> string -> thm -> thm val rule: thm -> thm end; @@ -25,7 +26,7 @@ val op ==> = Logic.mk_implies; -fun rule raw_surj_pair = +fun rule_params a b raw_surj_pair = let val ct = Thm.cterm_of (Thm.sign_of_thm raw_surj_pair); @@ -37,7 +38,7 @@ val P = Free (variant used "P", pT --> propT); (*"!!a b. PROP (a, b)"*) - val all_a_b = all "a" aT (all "b" bT (P $ (con $ Bound 1 $ Bound 0))); + val all_a_b = all a aT (all b bT (P $ (con $ Bound 1 $ Bound 0))); (*"!!x. PROP P x"*) val all_x = all "x" pT (P $ Bound 0); @@ -57,5 +58,7 @@ (fn prems => [resolve_tac prems 1]); in standard (Thm.equal_intr lem4 lem3) end; +val rule = rule_params "a" "b"; + end;