# HG changeset patch # User ballarin # Date 1122994255 -7200 # Node ID 307b2ec590ffd5b7455cd74409e7fb7e52d01e83 # Parent e0050191e2d1c685bb43c8696924a6f23f4f17fc Turned simp_implies into binary operator. diff -r e0050191e2d1 -r 307b2ec590ff src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Aug 02 13:13:18 2005 +0200 +++ b/src/HOL/HOL.thy Tue Aug 02 16:50:55 2005 +0200 @@ -1124,13 +1124,19 @@ by (unfold Let_def) text {* -The following copy of the implication operator is useful for -fine-tuning congruence rules. + The following copy of the implication operator is useful for + fine-tuning congruence rules. It instructs the simplifier to simplify + its premise. *} consts - simp_implies :: "[prop, prop] => prop" ("(_/ =simp=> _)" [2, 1] 1) -defs simp_implies_def: "simp_implies \ op ==>" + "=simp=>" :: "[prop, prop] => prop" (infixr 1) +(* + "op =simp=>" :: "[prop, prop] => prop" ("(_/ =simp=> _)" [2, 1] 1) +syntax + "op =simp=>" :: "[prop, prop] => prop" ("op =simp=>") +*) +defs simp_implies_def: "op =simp=> \ op ==>" lemma simp_impliesI: assumes PQ: "(PROP P \ PROP Q)" diff -r e0050191e2d1 -r 307b2ec590ff src/HOL/simpdata.ML --- a/src/HOL/simpdata.ML Tue Aug 02 13:13:18 2005 +0200 +++ b/src/HOL/simpdata.ML Tue Aug 02 16:50:55 2005 +0200 @@ -208,7 +208,7 @@ fun lift_meta_eq_to_obj_eq i st = let val {sign, ...} = rep_thm st; - fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q + fun count_imp (Const ("HOL.op =simp=>", _) $ P $ Q) = 1 + count_imp Q | count_imp _ = 0; val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1))) in if j = 0 then meta_eq_to_obj_eq @@ -216,7 +216,7 @@ let val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j); fun mk_simp_implies Q = foldr (fn (R, S) => - Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps + Const ("HOL.op =simp=>", propT --> propT --> propT) $ R $ S) Q Ps val aT = TFree ("'a", HOLogic.typeS); val x = Free ("x", aT); val y = Free ("y", aT)