src/HOL/Tools/function_package/lexicographic_order.ML
changeset 24977 9f98751c9628
parent 24961 5298ee9c3fe5
child 25509 e537c91b043d
equal deleted inserted replaced
24976:821628d16552 24977:9f98751c9628
   213 (** Proof Reconstruction **)
   213 (** Proof Reconstruction **)
   214 
   214 
   215 (* prove row :: cell list -> tactic *)
   215 (* prove row :: cell list -> tactic *)
   216 fun prove_row (Less less_thm :: _) =
   216 fun prove_row (Less less_thm :: _) =
   217     (rtac @{thm "mlex_less"} 1)
   217     (rtac @{thm "mlex_less"} 1)
   218     THEN PRIMITIVE (flip implies_elim less_thm)
   218     THEN PRIMITIVE (Thm.elim_implies less_thm)
   219   | prove_row (LessEq (lesseq_thm, _) :: tail) =
   219   | prove_row (LessEq (lesseq_thm, _) :: tail) =
   220     (rtac @{thm "mlex_leq"} 1)
   220     (rtac @{thm "mlex_leq"} 1)
   221     THEN PRIMITIVE (flip implies_elim lesseq_thm)
   221     THEN PRIMITIVE (Thm.elim_implies lesseq_thm)
   222     THEN prove_row tail
   222     THEN prove_row tail
   223   | prove_row _ = sys_error "lexicographic_order"
   223   | prove_row _ = sys_error "lexicographic_order"
   224 
   224 
   225 
   225 
   226 (** Error reporting **)
   226 (** Error reporting **)