(* Title: HOL/Prolog/HOHH.thy
ID: $Id$
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
header {* Higher-order hereditary Harrop formulas *}
theory HOHH
imports HOL
begin
consts
(* D-formulas (programs): D ::= !x. D | D .. D | D :- G | A *)
"Dand" :: "[bool, bool] => bool" (infixr ".." 28)
":-" :: "[bool, bool] => bool" (infixl 29)
(* G-formulas (goals): G ::= A | G & G | G | G | ? x. G
| True | !x. G | D => G *)
(*"," :: "[bool, bool] => bool" (infixr 35)*)
"=>" :: "[bool, bool] => bool" (infixr 27)
translations
"D :- G" => "G --> D"
"D1 .. D2" => "D1 & D2"
(*"G1 , G2" => "G1 & G2"*)
"D => G" => "D --> G"
end