src/HOL/NSA/NSComplex.thy
changeset 42463 f270e3e18be5
parent 41959 b460124855b8
child 44711 cd8dbfc272df
     1.1 --- a/src/HOL/NSA/NSComplex.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/NSA/NSComplex.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports Complex NSA
     1.5  begin
     1.6  
     1.7 -types hcomplex = "complex star"
     1.8 +type_synonym hcomplex = "complex star"
     1.9  
    1.10  abbreviation
    1.11    hcomplex_of_complex :: "complex => complex star" where