simp_implies: proper named infix;
authorwenzelm
Wed Aug 31 15:46:34 2005 +0200 (2005-08-31)
changeset 17197917c6e7ca28d
parent 17196 d26778f3e6dd
child 17198 ffe8efe856e3
simp_implies: proper named infix;
src/HOL/HOL.thy
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Aug 31 15:46:33 2005 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Aug 31 15:46:34 2005 +0200
     1.3 @@ -1129,14 +1129,9 @@
     1.4    its premise.
     1.5  *}
     1.6  
     1.7 -consts
     1.8 -  "=simp=>" :: "[prop, prop] => prop"  (infixr 1)
     1.9 -(*
    1.10 -  "op =simp=>" :: "[prop, prop] => prop"  ("(_/ =simp=> _)" [2, 1] 1)
    1.11 -syntax
    1.12 -  "op =simp=>" :: "[prop, prop] => prop"  ("op =simp=>")
    1.13 -*)
    1.14 -defs simp_implies_def: "op =simp=> \<equiv> op ==>"
    1.15 +constdefs
    1.16 +  simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1)
    1.17 +  "simp_implies \<equiv> op ==>"
    1.18  
    1.19  lemma simp_impliesI: 
    1.20    assumes PQ: "(PROP P \<Longrightarrow> PROP Q)"
     2.1 --- a/src/HOL/simpdata.ML	Wed Aug 31 15:46:33 2005 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Wed Aug 31 15:46:34 2005 +0200
     2.3 @@ -208,7 +208,7 @@
     2.4  fun lift_meta_eq_to_obj_eq i st =
     2.5    let
     2.6      val {sign, ...} = rep_thm st;
     2.7 -    fun count_imp (Const ("HOL.op =simp=>", _) $ P $ Q) = 1 + count_imp Q
     2.8 +    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
     2.9        | count_imp _ = 0;
    2.10      val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
    2.11    in if j = 0 then meta_eq_to_obj_eq
    2.12 @@ -216,7 +216,7 @@
    2.13        let
    2.14          val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
    2.15          fun mk_simp_implies Q = foldr (fn (R, S) =>
    2.16 -          Const ("HOL.op =simp=>", propT --> propT --> propT) $ R $ S) Q Ps
    2.17 +          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
    2.18          val aT = TFree ("'a", HOLogic.typeS);
    2.19          val x = Free ("x", aT);
    2.20          val y = Free ("y", aT)