src/Sequents/S4.thy
changeset 39159 0dec18004e75
parent 35762 af3ff2ba4c54
child 42814 5af15f1e2ef6
     1.1 --- a/src/Sequents/S4.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/Sequents/S4.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -34,12 +34,12 @@
     1.4  ML {*
     1.5  structure S4_Prover = Modal_ProverFun
     1.6  (
     1.7 -  val rewrite_rls = thms "rewrite_rls"
     1.8 -  val safe_rls = thms "safe_rls"
     1.9 -  val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"]
    1.10 -  val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
    1.11 -  val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
    1.12 -    thm "rstar1", thm "rstar2"]
    1.13 +  val rewrite_rls = @{thms rewrite_rls}
    1.14 +  val safe_rls = @{thms safe_rls}
    1.15 +  val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}]
    1.16 +  val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
    1.17 +  val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
    1.18 +    @{thm rstar1}, @{thm rstar2}]
    1.19  )
    1.20  *}
    1.21