src/HOL/Word/TdThs.thy
changeset 30729 461ee3e49ad3
parent 29631 3aa049e5f156
child 30952 7ab2716dd93b
--- a/src/HOL/Word/TdThs.thy	Thu Mar 26 19:24:21 2009 +0100
+++ b/src/HOL/Word/TdThs.thy	Thu Mar 26 20:08:55 2009 +0100
@@ -89,7 +89,7 @@
 
 end
 
-interpretation nat_int!: type_definition int nat "Collect (op <= 0)"
+interpretation nat_int: type_definition int nat "Collect (op <= 0)"
   by (rule td_nat_int)
 
 declare