(*
mint.thy - modal -> intuitionistic logic
Intuitionistic Logic, as per Gore, TR-ARP-1-95
(roughly - changed to define ->h and ~h in terms of
related logical connectives *)
mint = S4 +
rules
(* important - this rule only applies to intuitionistic formulae *)
pshA "A |- $X ==> @A |- $X"
consts
(* Logical Connectives for Intuitionistic Logic *)
"~h" :: "formula => formula" ("~h _" [70] 70)
"->h" :: "[formula, formula] => formula" ("(_ ->h _)" [64, 63] 63)
defs
noth_def "~h x == wbx (~ x)"
imph_def "x ->h y == wbx (x -> y)"
end