# HG changeset patch
# User wenzelm
# Date 1265925316 -3600
# Node ID b1fd1d756e208da4d9042998a096bb7f8cc3d0e6
# Parent  1a0c129bb2e003c0d14edabd4c2c923f69437b1a
formal markup of @{syntax_const} and @{const_syntax};
authentic syntax for extra robustness;

diff -r 1a0c129bb2e0 -r b1fd1d756e20 src/HOL/Statespace/StateFun.thy
--- a/src/HOL/Statespace/StateFun.thy	Thu Feb 11 22:19:58 2010 +0100
+++ b/src/HOL/Statespace/StateFun.thy	Thu Feb 11 22:55:16 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      StateFun.thy
-    ID:         $Id$
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
@@ -34,12 +33,12 @@
 lemma K_statefun_cong [cong]: "K_statefun c x = K_statefun c x"
   by (rule refl)
 
-constdefs lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
-"lookup destr n s \<equiv> destr (s n)"
+definition lookup:: "('v \<Rightarrow> 'a) \<Rightarrow> 'n \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> 'a"
+  where "lookup destr n s = destr (s n)"
 
-constdefs update:: 
+definition update::
   "('v \<Rightarrow> 'a1) \<Rightarrow> ('a2 \<Rightarrow> 'v) \<Rightarrow> 'n \<Rightarrow> ('a1 \<Rightarrow> 'a2) \<Rightarrow> ('n \<Rightarrow> 'v) \<Rightarrow> ('n \<Rightarrow> 'v)"
-"update destr constr n f s \<equiv> s(n := constr (f (destr (s n))))"
+  where "update destr constr n f s = s(n := constr (f (destr (s n))))"
 
 lemma lookup_update_same:
   "(\<And>v. destr (constr v) = v) \<Longrightarrow> lookup destr n (update destr constr n f s) = 
diff -r 1a0c129bb2e0 -r b1fd1d756e20 src/HOL/Statespace/StateSpaceSyntax.thy
--- 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