src/HOL/Statespace/StateSpaceSyntax.thy
changeset 52143 36ffe23b25f8
parent 41959 b460124855b8
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/Statespace/StateSpaceSyntax.thy	Sat May 25 15:00:53 2013 +0200
     1.2 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Sat May 25 15:37:53 2013 +0200
     1.3 @@ -21,14 +21,14 @@
     1.4    "s<x:=y>" == "_statespace_update s x y"
     1.5  
     1.6  
     1.7 -parse_translation (advanced)
     1.8 +parse_translation
     1.9  {*
    1.10   [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
    1.11    (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
    1.12  *}
    1.13  
    1.14  
    1.15 -print_translation (advanced)
    1.16 +print_translation
    1.17  {*
    1.18   [(@{const_syntax lookup}, StateSpace.lookup_tr'),
    1.19    (@{const_syntax update}, StateSpace.update_tr')]