src/HOL/Statespace/StateSpaceSyntax.thy
changeset 35114 b1fd1d756e20
parent 25171 4a9c25bffc9b
child 38838 62f6ba39b3d4
--- a/src/HOL/Statespace/StateSpaceSyntax.thy	Thu Feb 11 22:19:58 2010 +0100
+++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Thu Feb 11 22:55:16 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      StateSpaceSyntax.thy
-    ID:         $Id$
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -13,30 +12,27 @@
 can choose if you want to use it or not.  *}
 
 syntax 
- "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" ("_\<cdot>_" [60,60] 60)
- "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
- "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_<_>" [900,0] 900)
+  "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
+  "_statespace_update" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> ('a \<Rightarrow> 'b)"
+  "_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)"  ("_<_>" [900, 0] 900)
 
 translations
-  "_statespace_updates f (_updbinds b bs)"  == 
-     "_statespace_updates (_statespace_updates f b) bs"
-  "s<x:=y>"                     == "_statespace_update s x y"
+  "_statespace_updates f (_updbinds b bs)" ==
+    "_statespace_updates (_statespace_updates f b) bs"
+  "s<x:=y>" == "_statespace_update s x y"
 
 
 parse_translation (advanced)
 {*
-[("_statespace_lookup",StateSpace.lookup_tr),
- ("_get",StateSpace.lookup_tr),
- ("_statespace_update",StateSpace.update_tr)] 
+ [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
+  (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
 *}
 
 
 print_translation (advanced)
 {*
-[("lookup",StateSpace.lookup_tr'),
- ("StateFun.lookup",StateSpace.lookup_tr'),
- ("update",StateSpace.update_tr'),
- ("StateFun.update",StateSpace.update_tr')] 
+ [(@{const_syntax lookup}, StateSpace.lookup_tr'),
+  (@{const_syntax update}, StateSpace.update_tr')]
 *}
 
-end
\ No newline at end of file
+end