--- a/src/Sequents/S4.thy Thu Jul 23 14:20:51 2015 +0200
+++ b/src/Sequents/S4.thy Thu Jul 23 14:25:05 2015 +0200
@@ -31,7 +31,7 @@
"[| $E |L> $E'; $F |L> $F'; $G |R> $G';
$E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G"
-ML {*
+ML \<open>
structure S4_Prover = Modal_ProverFun
(
val rewrite_rls = @{thms rewrite_rls}
@@ -41,10 +41,10 @@
val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
@{thm rstar1}, @{thm rstar2}]
)
-*}
+\<close>
method_setup S4_solve =
- {* Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2)) *}
+ \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (S4_Prover.solve_tac ctxt 2))\<close>
(* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)