# HG changeset patch
# User haftmann
# Date 1263658527 -3600
# Node ID 44294cfecb1d1ac107ad434d4cf854ba4df99cac
# Parent  bb9dad7de5151a7a057812628a4efb88fc1a387e
modernized syntax

diff -r bb9dad7de515 -r 44294cfecb1d src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Fri Jan 15 08:27:21 2010 +0100
+++ b/src/HOL/Bali/Table.thy	Sat Jan 16 17:15:27 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Bali/Table.thy
-    ID:         $Id$
     Author:     David von Oheimb
 *)
 header {* Abstract tables and their implementation as lists *}
@@ -41,9 +40,10 @@
 syntax
   table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"   --{* concrete table *}
   
+abbreviation
+  "table_of \<equiv> map_of"
+
 translations
-  "table_of" == "map_of"
-  
   (type)"'a \<rightharpoonup> 'b"       <= (type)"'a \<Rightarrow> 'b Datatype.option"
   (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"