# HG changeset patch
# User wenzelm
# Date 1192195272 -7200
# Node ID 60e5516c7b06662ba416149911c82ef7b24103fa
# Parent  c62c5209487b340c744289c6df6dad751608318b
replaced syntax/translations by abbreviation;

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 \<times> int"
-syntax "_Num0" :: "Num" ("0\<^sub>N")
-translations "0\<^sub>N" \<rightleftharpoons> "(0, 0)"
-syntax "_Numi" :: "int \<Rightarrow> Num" ("_\<^sub>N")
-translations "i\<^sub>N" \<rightleftharpoons> "(i, 1) \<Colon> Num"
+
+abbreviation
+  Num0_syn :: Num ("0\<^sub>N")
+where "0\<^sub>N \<equiv> (0, 0)"
+
+abbreviation
+  Numi_syn :: "int \<Rightarrow> Num" ("_\<^sub>N")
+where "i\<^sub>N \<equiv> (i, 1)"
 
 definition
   isnormNum :: "Num \<Rightarrow> bool"
@@ -131,8 +135,8 @@
 qed
 
 lemma Ninv_normN[simp]: "isnormNum x \<Longrightarrow> 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 \<noteq> 0 \<Longrightarrow> isnormNum i\<^sub>N"