src/HOL/Prolog/HOHH.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 9015 8006e9009621
child 13208 965f95a3abd9
permissions -rw-r--r--
improved theory reference in comment
     1 (* higher-order hereditary Harrop formulas *)
     2 
     3 HOHH = HOL +
     4 
     5 consts
     6 
     7 (* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A		*)
     8   "Dand"	:: [bool, bool] => bool		(infixr ".." 28)
     9   ":-"		:: [bool, bool] => bool		(infixl 29)
    10 
    11 (* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G 
    12 			       | True | !x. G | D => G			*)
    13 (*","           :: [bool, bool] => bool		(infixr 35)*)
    14   "=>"		:: [bool, bool] => bool		(infixr 27)
    15 
    16 translations
    17 
    18   "D :- G"	=>	"G --> D"
    19   "D1 .. D2"	=>	"D1 & D2"
    20 (*"G1 , G2"	=>	"G1 & G2"*)
    21   "D => G"	=>	"D --> G"
    22 
    23 end
    24