replaced (flip Thm.implies_elim) by Thm.elim_implies;
authorwenzelm
Thu Oct 11 19:10:19 2007 +0200 (2007-10-11)
changeset 249779f98751c9628
parent 24976 821628d16552
child 24978 159b0f4dd1e9
replaced (flip Thm.implies_elim) by Thm.elim_implies;
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/mutual.ML
     1.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Thu Oct 11 19:10:17 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Thu Oct 11 19:10:19 2007 +0200
     1.3 @@ -196,7 +196,7 @@
     1.4  
     1.5  fun import_thm thy (fixes, athms) =
     1.6      fold (forall_elim o cterm_of thy o Free) fixes
     1.7 - #> fold (flip implies_elim) athms
     1.8 + #> fold Thm.elim_implies athms
     1.9  
    1.10  fun assume_in_ctxt thy (fixes, athms) prop =
    1.11      let
     2.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Thu Oct 11 19:10:17 2007 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Thu Oct 11 19:10:19 2007 +0200
     2.3 @@ -204,15 +204,15 @@
     2.4          val lGI = GIntro_thm
     2.5                      |> forall_elim (cert f)
     2.6                      |> fold forall_elim cqs
     2.7 -                    |> fold (flip implies_elim) ags
     2.8 +                    |> fold Thm.elim_implies ags
     2.9  
    2.10          fun mk_call_info (rcfix, rcassm, rcarg) RI =
    2.11              let
    2.12                  val llRI = RI
    2.13                               |> fold forall_elim cqs
    2.14                               |> fold (forall_elim o cert o Free) rcfix
    2.15 -                             |> fold (flip implies_elim) ags
    2.16 -                             |> fold (flip implies_elim) rcassm
    2.17 +                             |> fold Thm.elim_implies ags
    2.18 +                             |> fold Thm.elim_implies rcassm
    2.19  
    2.20                  val h_assum =
    2.21                      HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
    2.22 @@ -271,9 +271,9 @@
    2.23           in
    2.24             compat         (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
    2.25                  |> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *)
    2.26 -                |> fold (flip implies_elim) agsj
    2.27 -                |> fold (flip implies_elim) agsi
    2.28 -                |> flip implies_elim ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
    2.29 +                |> fold Thm.elim_implies agsj
    2.30 +                |> fold Thm.elim_implies agsi
    2.31 +                |> Thm.elim_implies ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *)
    2.32           end
    2.33         else
    2.34           let
    2.35 @@ -281,9 +281,9 @@
    2.36           in
    2.37                 compat        (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
    2.38                   |> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *)
    2.39 -                 |> fold (flip implies_elim) agsi
    2.40 -                 |> fold (flip implies_elim) agsj
    2.41 -                 |> flip implies_elim (assume lhsi_eq_lhsj)
    2.42 +                 |> fold Thm.elim_implies agsi
    2.43 +                 |> fold Thm.elim_implies agsj
    2.44 +                 |> Thm.elim_implies (assume lhsi_eq_lhsj)
    2.45                   |> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *)
    2.46           end
    2.47      end
    2.48 @@ -331,8 +331,8 @@
    2.49  
    2.50          val RLj_import = 
    2.51              RLj |> fold forall_elim cqsj'
    2.52 -                |> fold (flip implies_elim) agsj'
    2.53 -                |> fold (flip implies_elim) Ghsj'
    2.54 +                |> fold Thm.elim_implies agsj'
    2.55 +                |> fold Thm.elim_implies Ghsj'
    2.56  
    2.57          val y_eq_rhsj'h = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h))))
    2.58          val lhsi_eq_lhsj' = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *)
    2.59 @@ -373,8 +373,8 @@
    2.60                             |> forall_elim (cterm_of thy lhs)
    2.61                             |> forall_elim (cterm_of thy y)
    2.62                             |> forall_elim P
    2.63 -                           |> flip implies_elim G_lhs_y
    2.64 -                           |> fold (flip implies_elim) unique_clauses
    2.65 +                           |> Thm.elim_implies G_lhs_y
    2.66 +                           |> fold Thm.elim_implies unique_clauses
    2.67                             |> implies_intr (cprop_of G_lhs_y)
    2.68                             |> forall_intr (cterm_of thy y)
    2.69  
    2.70 @@ -612,7 +612,7 @@
    2.71            
    2.72      fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
    2.73          sih |> forall_elim (cterm_of thy rcarg)
    2.74 -            |> flip implies_elim llRI
    2.75 +            |> Thm.elim_implies llRI
    2.76              |> fold_rev (implies_intr o cprop_of) CCas
    2.77              |> fold_rev (forall_intr o cterm_of thy o Free) RIvs
    2.78          
    2.79 @@ -627,9 +627,9 @@
    2.80           
    2.81      val P_lhs = assume step
    2.82             |> fold forall_elim cqs
    2.83 -           |> flip implies_elim lhs_D 
    2.84 -           |> fold (flip implies_elim) ags
    2.85 -           |> fold (flip implies_elim) P_recs
    2.86 +           |> Thm.elim_implies lhs_D 
    2.87 +           |> fold Thm.elim_implies ags
    2.88 +           |> fold Thm.elim_implies P_recs
    2.89            
    2.90      val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
    2.91             |> Simplifier.rewrite replace_x_ss
    2.92 @@ -728,9 +728,9 @@
    2.93                        
    2.94              val thm = assume hyp
    2.95                        |> fold forall_elim cqs
    2.96 -                      |> fold (flip implies_elim) ags
    2.97 +                      |> fold Thm.elim_implies ags
    2.98                        |> FundefCtxTree.import_thm thy (fixes, assumes) (*  "(arg, lhs) : R'"  *)
    2.99 -                      |> fold (flip implies_elim) used
   2.100 +                      |> fold Thm.elim_implies used
   2.101                        
   2.102              val acc = thm COMP ih_case
   2.103                        
     3.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 11 19:10:17 2007 +0200
     3.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 11 19:10:19 2007 +0200
     3.3 @@ -202,7 +202,7 @@
     3.4  
     3.5        val t' = new_subg
     3.6                  |> fold forall_elim cps
     3.7 -                |> flip implies_elim (fold forall_elim cps sg2)
     3.8 +                |> Thm.elim_implies (fold forall_elim cps sg2)
     3.9                  |> fold_rev forall_intr cps
    3.10  
    3.11        val st' = implies_elim st t'
     4.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Oct 11 19:10:17 2007 +0200
     4.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Thu Oct 11 19:10:19 2007 +0200
     4.3 @@ -215,10 +215,10 @@
     4.4  (* prove row :: cell list -> tactic *)
     4.5  fun prove_row (Less less_thm :: _) =
     4.6      (rtac @{thm "mlex_less"} 1)
     4.7 -    THEN PRIMITIVE (flip implies_elim less_thm)
     4.8 +    THEN PRIMITIVE (Thm.elim_implies less_thm)
     4.9    | prove_row (LessEq (lesseq_thm, _) :: tail) =
    4.10      (rtac @{thm "mlex_leq"} 1)
    4.11 -    THEN PRIMITIVE (flip implies_elim lesseq_thm)
    4.12 +    THEN PRIMITIVE (Thm.elim_implies lesseq_thm)
    4.13      THEN prove_row tail
    4.14    | prove_row _ = sys_error "lexicographic_order"
    4.15  
     5.1 --- a/src/HOL/Tools/function_package/mutual.ML	Thu Oct 11 19:10:17 2007 +0200
     5.2 +++ b/src/HOL/Tools/function_package/mutual.ML	Thu Oct 11 19:10:19 2007 +0200
     5.3 @@ -221,7 +221,7 @@
     5.4        val ags = map (assume o cterm_of thy) gs
     5.5  
     5.6        val import = fold forall_elim cqs
     5.7 -                   #> fold (flip implies_elim) ags
     5.8 +                   #> fold Thm.elim_implies ags
     5.9  
    5.10        val export = fold_rev (implies_intr o cprop_of) ags
    5.11                     #> fold_rev forall_intr_rename (oqnames ~~ cqs)