# HG changeset patch
# User wenzelm
# Date 1125495994 -7200
# Node ID 917c6e7ca28d416ab69a7ffcb48d5c5ec66951d7
# Parent  d26778f3e6dd2013484a42297f2713e9d95ce271
simp_implies: proper named infix;

diff -r d26778f3e6dd -r 917c6e7ca28d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 31 15:46:33 2005 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 31 15:46:34 2005 +0200
@@ -1129,14 +1129,9 @@
   its premise.
 *}
 
-consts
-  "=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 ==>"
+constdefs
+  simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1)
+  "simp_implies \<equiv> op ==>"
 
 lemma simp_impliesI: 
   assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
diff -r d26778f3e6dd -r 917c6e7ca28d src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Aug 31 15:46:33 2005 +0200
+++ b/src/HOL/simpdata.ML	Wed Aug 31 15:46:34 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.op =simp=>", _) $ P $ Q) = 1 + count_imp Q
+    fun count_imp (Const ("HOL.simp_implies", _) $ 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.op =simp=>", propT --> propT --> propT) $ R $ S) Q Ps
+          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
         val aT = TFree ("'a", HOLogic.typeS);
         val x = Free ("x", aT);
         val y = Free ("y", aT)