Turned simp_implies into binary operator.
--- 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 \<equiv> 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=> \<equiv> op ==>"
lemma simp_impliesI:
assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
--- 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)