# HG changeset patch # User wenzelm # Date 1192122619 -7200 # Node ID 9f98751c96281864b8ee8ea089662be588274a4d # Parent 821628d165524ffd59d7942b425028ff21f0100e replaced (flip Thm.implies_elim) by Thm.elim_implies; diff -r 821628d16552 -r 9f98751c9628 src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Thu Oct 11 19:10:17 2007 +0200 +++ b/src/HOL/Tools/function_package/context_tree.ML Thu Oct 11 19:10:19 2007 +0200 @@ -196,7 +196,7 @@ fun import_thm thy (fixes, athms) = fold (forall_elim o cterm_of thy o Free) fixes - #> fold (flip implies_elim) athms + #> fold Thm.elim_implies athms fun assume_in_ctxt thy (fixes, athms) prop = let diff -r 821628d16552 -r 9f98751c9628 src/HOL/Tools/function_package/fundef_core.ML --- a/src/HOL/Tools/function_package/fundef_core.ML Thu Oct 11 19:10:17 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_core.ML Thu Oct 11 19:10:19 2007 +0200 @@ -204,15 +204,15 @@ val lGI = GIntro_thm |> forall_elim (cert f) |> fold forall_elim cqs - |> fold (flip implies_elim) ags + |> fold Thm.elim_implies ags fun mk_call_info (rcfix, rcassm, rcarg) RI = let val llRI = RI |> fold forall_elim cqs |> fold (forall_elim o cert o Free) rcfix - |> fold (flip implies_elim) ags - |> fold (flip implies_elim) rcassm + |> fold Thm.elim_implies ags + |> fold Thm.elim_implies rcassm val h_assum = HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) @@ -271,9 +271,9 @@ in compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) - |> fold (flip implies_elim) agsj - |> fold (flip implies_elim) agsi - |> flip implies_elim ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) + |> fold Thm.elim_implies agsj + |> fold Thm.elim_implies agsi + |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) end else let @@ -281,9 +281,9 @@ in compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) - |> fold (flip implies_elim) agsi - |> fold (flip implies_elim) agsj - |> flip implies_elim (assume lhsi_eq_lhsj) + |> fold Thm.elim_implies agsi + |> fold Thm.elim_implies agsj + |> Thm.elim_implies (assume lhsi_eq_lhsj) |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) end end @@ -331,8 +331,8 @@ val RLj_import = RLj |> fold forall_elim cqsj' - |> fold (flip implies_elim) agsj' - |> fold (flip implies_elim) Ghsj' + |> fold Thm.elim_implies agsj' + |> fold Thm.elim_implies Ghsj' val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) @@ -373,8 +373,8 @@ |> forall_elim (cterm_of thy lhs) |> forall_elim (cterm_of thy y) |> forall_elim P - |> flip implies_elim G_lhs_y - |> fold (flip implies_elim) unique_clauses + |> Thm.elim_implies G_lhs_y + |> fold Thm.elim_implies unique_clauses |> implies_intr (cprop_of G_lhs_y) |> forall_intr (cterm_of thy y) @@ -612,7 +612,7 @@ fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih |> forall_elim (cterm_of thy rcarg) - |> flip implies_elim llRI + |> Thm.elim_implies llRI |> fold_rev (implies_intr o cprop_of) CCas |> fold_rev (forall_intr o cterm_of thy o Free) RIvs @@ -627,9 +627,9 @@ val P_lhs = assume step |> fold forall_elim cqs - |> flip implies_elim lhs_D - |> fold (flip implies_elim) ags - |> fold (flip implies_elim) P_recs + |> Thm.elim_implies lhs_D + |> fold Thm.elim_implies ags + |> fold Thm.elim_implies P_recs val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) |> Simplifier.rewrite replace_x_ss @@ -728,9 +728,9 @@ val thm = assume hyp |> fold forall_elim cqs - |> fold (flip implies_elim) ags + |> fold Thm.elim_implies ags |> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *) - |> fold (flip implies_elim) used + |> fold Thm.elim_implies used val acc = thm COMP ih_case diff -r 821628d16552 -r 9f98751c9628 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Thu Oct 11 19:10:17 2007 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Oct 11 19:10:19 2007 +0200 @@ -202,7 +202,7 @@ val t' = new_subg |> fold forall_elim cps - |> flip implies_elim (fold forall_elim cps sg2) + |> Thm.elim_implies (fold forall_elim cps sg2) |> fold_rev forall_intr cps val st' = implies_elim st t' diff -r 821628d16552 -r 9f98751c9628 src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Thu Oct 11 19:10:17 2007 +0200 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Thu Oct 11 19:10:19 2007 +0200 @@ -215,10 +215,10 @@ (* prove row :: cell list -> tactic *) fun prove_row (Less less_thm :: _) = (rtac @{thm "mlex_less"} 1) - THEN PRIMITIVE (flip implies_elim less_thm) + THEN PRIMITIVE (Thm.elim_implies less_thm) | prove_row (LessEq (lesseq_thm, _) :: tail) = (rtac @{thm "mlex_leq"} 1) - THEN PRIMITIVE (flip implies_elim lesseq_thm) + THEN PRIMITIVE (Thm.elim_implies lesseq_thm) THEN prove_row tail | prove_row _ = sys_error "lexicographic_order" diff -r 821628d16552 -r 9f98751c9628 src/HOL/Tools/function_package/mutual.ML --- a/src/HOL/Tools/function_package/mutual.ML Thu Oct 11 19:10:17 2007 +0200 +++ b/src/HOL/Tools/function_package/mutual.ML Thu Oct 11 19:10:19 2007 +0200 @@ -221,7 +221,7 @@ val ags = map (assume o cterm_of thy) gs val import = fold forall_elim cqs - #> fold (flip implies_elim) ags + #> fold Thm.elim_implies ags val export = fold_rev (implies_intr o cprop_of) ags #> fold_rev forall_intr_rename (oqnames ~~ cqs)