src/Sequents/Modal0.thy
changeset 35113 1a0c129bb2e0
parent 21426 87ac12bed1ab
child 48891 c0eafbd55de3
--- a/src/Sequents/Modal0.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/Sequents/Modal0.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Sequents/Modal0.thy
-    ID:         $Id$
     Author:     Martin Coen
     Copyright   1991  University of Cambridge
 *)
@@ -18,21 +17,23 @@
   Rstar         :: "two_seqi"
 
 syntax
-  "@Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
-  "@Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
+  "_Lstar"      :: "two_seqe"   ("(_)|L>(_)" [6,6] 5)
+  "_Rstar"      :: "two_seqe"   ("(_)|R>(_)" [6,6] 5)
 
 ML {*
-  val Lstar = "Lstar";
-  val Rstar = "Rstar";
-  val SLstar = "@Lstar";
-  val SRstar = "@Rstar";
-
-  fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
-  fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
+  fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2;
+  fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2;
 *}
 
-parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
-print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
+parse_translation {*
+ [(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}),
+  (@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})]
+*}
+
+print_translation {*
+ [(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}),
+  (@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})]
+*}
 
 defs
   strimp_def:    "P --< Q == [](P --> Q)"