src/HOL/Prolog/HOHH.thy
author oheimb
Tue Jun 11 16:43:17 2002 +0200 (2002-06-11)
changeset 13208 965f95a3abd9
parent 9015 8006e9009621
child 14981 e73f8140af78
permissions -rw-r--r--
added the usual file headers
     1 (*  Title:    HOL/Prolog/HOHH.thy
     2     ID:       $Id$
     3     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4     License:  GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 higher-order hereditary Harrop formulas 
     7 *)
     8 
     9 HOHH = HOL +
    10 
    11 consts
    12 
    13 (* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A		*)
    14   "Dand"	:: [bool, bool] => bool		(infixr ".." 28)
    15   ":-"		:: [bool, bool] => bool		(infixl 29)
    16 
    17 (* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G 
    18 			       | True | !x. G | D => G			*)
    19 (*","           :: [bool, bool] => bool		(infixr 35)*)
    20   "=>"		:: [bool, bool] => bool		(infixr 27)
    21 
    22 translations
    23 
    24   "D :- G"	=>	"G --> D"
    25   "D1 .. D2"	=>	"D1 & D2"
    26 (*"G1 , G2"	=>	"G1 & G2"*)
    27   "D => G"	=>	"D --> G"
    28 
    29 end
    30