src/Sequents/S43.thy
changeset 60770 240563fbf41d
parent 54742 7a86358a3c0b
child 61385 538100cc4399
--- a/src/Sequents/S43.thy	Thu Jul 23 14:20:51 2015 +0200
+++ b/src/Sequents/S43.thy	Thu Jul 23 14:25:05 2015 +0200
@@ -16,21 +16,21 @@
   "_S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
                          ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
 
-parse_translation {*
+parse_translation \<open>
   let
     val tr  = seq_tr;
     fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
       Const (@{const_syntax S43pi}, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
   in [(@{syntax_const "_S43pi"}, K s43pi_tr)] end
-*}
+\<close>
 
-print_translation {*
+print_translation \<open>
 let
   val tr' = seq_tr';
   fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
     Const(@{syntax_const "_S43pi"}, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
 in [(@{const_syntax S43pi}, K s43pi_tr')] end
-*}
+\<close>
 
 axiomatization where
 (* Definition of the star operation using a set of Horn clauses  *)
@@ -76,7 +76,7 @@
    $L |- $R1, []P, $R2"
 
 
-ML {*
+ML \<open>
 structure S43_Prover = Modal_ProverFun
 (
   val rewrite_rls = @{thms rewrite_rls}
@@ -86,13 +86,13 @@
   val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
     @{thm rstar1}, @{thm rstar2}, @{thm S43pi0}, @{thm S43pi1}, @{thm S43pi2}]
 )
-*}
+\<close>
 
 
-method_setup S43_solve = {*
+method_setup S43_solve = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD
     (S43_Prover.solve_tac ctxt 2 ORELSE S43_Prover.solve_tac ctxt 3))
-*}
+\<close>
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)