src/HOL/MicroJava/J/JBasis.thy
changeset 10042 7164dc0d24d8
parent 8116 759f712f8f06
child 11026 a50365d21144
     1.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 -  unique  :: "('a \\<times> 'b) list \\<Rightarrow> bool"
     1.8 - "unique  \\<equiv> nodups \\<circ> map fst"
     1.9 +  unique  :: "('a \\<times> 'b) list => bool"
    1.10 + "unique  == nodups \\<circ> map fst"
    1.11  
    1.12  end