(* SSLer.thy
exponential restriction at logical level
*)
SSLer = SSer + SSL +
consts
"bang" :: "formula => formula" ("! _" [71] 71)
"query" :: "formula => formula" ("? _" [71] 71)
rules
(* exponential restriction rules at logical level *)
erbang "iser !A"
derquery "isder ? A"
(* rules for exponentials, s10.3, Fig 9 *)
queryA "[| A |- $Y ; isder $Y |] ==> ? A |- $Y"
queryS "$X |- A ==> $X |- ? A"
bangA "A |- $X ==> ! A |- $X"
bangS "[| $Y |- A ; iser $Y |] ==> $Y |- ! A"
end