src/HOL/ex/Tree23.thy
changeset 42463 f270e3e18be5
parent 33436 0b5f07dd68f5
child 45325 26b6179b5a45
     1.1 --- a/src/HOL/ex/Tree23.thy	Fri Apr 22 15:57:43 2011 +0200
     1.2 +++ b/src/HOL/ex/Tree23.thy	Sat Apr 23 13:00:19 2011 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  function definitions take a few minutes and can also be seen as stress tests
     1.5  for the function definition facility.  *}
     1.6  
     1.7 -types key = int -- {*for simplicity, should be a type class*}
     1.8 +type_synonym key = int -- {*for simplicity, should be a type class*}
     1.9  
    1.10  datatype ord = LESS | EQUAL | GREATER
    1.11