src/HOL/Bali/Table.thy
changeset 13337 f75dfc606ac7
parent 12925 99131847fb93
child 13585 db4005b40cc6
     1.1 --- a/src/HOL/Bali/Table.thy	Wed Jul 10 14:51:18 2002 +0200
     1.2 +++ b/src/HOL/Bali/Table.thy	Wed Jul 10 15:07:02 2002 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  syntax
     1.6    table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"    (* concrete table *)
     1.7 -
     1.8 +  
     1.9  translations
    1.10    "table_of" == "map_of"
    1.11