src/HOL/Statespace/StateSpaceSyntax.thy
changeset 63167 0909deb8059b
parent 58889 5b7a9633cfa8
child 69597 ff784d5a5bfb
     1.1 --- a/src/HOL/Statespace/StateSpaceSyntax.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/Statespace/StateSpaceSyntax.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -2,13 +2,13 @@
     1.4      Author:     Norbert Schirmer, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}*}
     1.8 +section \<open>Syntax for State Space Lookup and Update \label{sec:StateSpaceSyntax}\<close>
     1.9  theory StateSpaceSyntax
    1.10  imports StateSpaceLocale
    1.11  begin
    1.12  
    1.13 -text {* The state space syntax is kept in an extra theory so that you
    1.14 -can choose if you want to use it or not.  *}
    1.15 +text \<open>The state space syntax is kept in an extra theory so that you
    1.16 +can choose if you want to use it or not.\<close>
    1.17  
    1.18  syntax 
    1.19    "_statespace_lookup" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  ("_\<cdot>_" [60, 60] 60)
    1.20 @@ -22,16 +22,16 @@
    1.21  
    1.22  
    1.23  parse_translation
    1.24 -{*
    1.25 +\<open>
    1.26   [(@{syntax_const "_statespace_lookup"}, StateSpace.lookup_tr),
    1.27    (@{syntax_const "_statespace_update"}, StateSpace.update_tr)]
    1.28 -*}
    1.29 +\<close>
    1.30  
    1.31  
    1.32  print_translation
    1.33 -{*
    1.34 +\<open>
    1.35   [(@{const_syntax lookup}, StateSpace.lookup_tr'),
    1.36    (@{const_syntax update}, StateSpace.update_tr')]
    1.37 -*}
    1.38 +\<close>
    1.39  
    1.40  end