diff -r c62c5209487b -r 60e5516c7b06 src/HOL/Library/Abstract_Rat.thy --- a/src/HOL/Library/Abstract_Rat.thy Fri Oct 12 15:00:21 2007 +0200 +++ b/src/HOL/Library/Abstract_Rat.thy Fri Oct 12 15:21:12 2007 +0200 @@ -10,10 +10,14 @@ begin types Num = "int \ int" -syntax "_Num0" :: "Num" ("0\<^sub>N") -translations "0\<^sub>N" \ "(0, 0)" -syntax "_Numi" :: "int \ Num" ("_\<^sub>N") -translations "i\<^sub>N" \ "(i, 1) \ Num" + +abbreviation + Num0_syn :: Num ("0\<^sub>N") +where "0\<^sub>N \ (0, 0)" + +abbreviation + Numi_syn :: "int \ Num" ("_\<^sub>N") +where "i\<^sub>N \ (i, 1)" definition isnormNum :: "Num \ bool" @@ -131,8 +135,8 @@ qed lemma Ninv_normN[simp]: "isnormNum x \ isnormNum (Ninv x)" -by (simp add: Ninv_def isnormNum_def split_def) -(cases "fst x = 0",auto simp add: igcd_commute) + by (simp add: Ninv_def isnormNum_def split_def) + (cases "fst x = 0", auto simp add: igcd_commute) lemma isnormNum_int[simp]: "isnormNum 0\<^sub>N" "isnormNum (1::int)\<^sub>N" "i \ 0 \ isnormNum i\<^sub>N"