src/HOL/Prolog/HOHH.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Prolog/HOHH.thy	Fri Jun 02 12:44:04 2000 +0200
@@ -0,0 +1,24 @@
+(* higher-order hereditary Harrop formulas *)
+
+HOHH = HOL +
+
+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
+