theory i131123a
imports Complex_Main
begin

definition MFalse :: "prop" ("MFalse") where
  "MFalse == (!!P. PROP P)"

definition Hnot_try :: "prop => prop" where
  "Hnot_try P == (PROP P ==> MFalse)"
export_code Hnot_try in Scala file "i131123a.scala"
(*ERROR: No code equations for all*)
 
definition Hnot :: "prop => prop" where
  "Hnot P == (PROP P ==> False)"

value "Hnot(Trueprop False)"

export_code Hnot in Scala file "i131123a.scala"
export_code Hnot in Haskell file "."

end