src/HOL/Library/Abstract_Rat.thy
changeset 42463 f270e3e18be5
parent 41528 276078f01ada
child 44779 98d597c4193d
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  imports Complex_Main
     1.5  begin
     1.6  
     1.7 -types Num = "int \<times> int"
     1.8 +type_synonym Num = "int \<times> int"
     1.9  
    1.10  abbreviation
    1.11    Num0_syn :: Num ("0\<^sub>N")