replaced syntax/translations by abbreviation;
authorwenzelm
Fri Oct 12 15:21:12 2007 +0200 (2007-10-12)
changeset 2500560e5516c7b06
parent 25004 c62c5209487b
child 25006 fcf5a999d1c3
replaced syntax/translations by abbreviation;
src/HOL/Library/Abstract_Rat.thy
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Fri Oct 12 15:00:21 2007 +0200
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Fri Oct 12 15:21:12 2007 +0200
     1.3 @@ -10,10 +10,14 @@
     1.4  begin
     1.5  
     1.6  types Num = "int \<times> int"
     1.7 -syntax "_Num0" :: "Num" ("0\<^sub>N")
     1.8 -translations "0\<^sub>N" \<rightleftharpoons> "(0, 0)"
     1.9 -syntax "_Numi" :: "int \<Rightarrow> Num" ("_\<^sub>N")
    1.10 -translations "i\<^sub>N" \<rightleftharpoons> "(i, 1) \<Colon> Num"
    1.11 +
    1.12 +abbreviation
    1.13 +  Num0_syn :: Num ("0\<^sub>N")
    1.14 +where "0\<^sub>N \<equiv> (0, 0)"
    1.15 +
    1.16 +abbreviation
    1.17 +  Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N")
    1.18 +where "i\<^sub>N \<equiv> (i, 1)"
    1.19  
    1.20  definition
    1.21    isnormNum :: "Num \<Rightarrow> bool"
    1.22 @@ -131,8 +135,8 @@
    1.23  qed
    1.24  
    1.25  lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> isnormNum (Ninv x)"
    1.26 -by (simp add: Ninv_def isnormNum_def split_def)
    1.27 -(cases "fst x = 0",auto simp add: igcd_commute)
    1.28 +  by (simp add: Ninv_def isnormNum_def split_def)
    1.29 +    (cases "fst x = 0", auto simp add: igcd_commute)
    1.30  
    1.31  lemma isnormNum_int[simp]: 
    1.32    "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"