src/HOL/Prolog/HOHH.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 14981 e73f8140af78
child 17311 5b1d47d920ce
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
     1 (*  Title:    HOL/Prolog/HOHH.thy
     2     ID:       $Id$
     3     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
     4 
     5 higher-order hereditary Harrop formulas 
     6 *)
     7 
     8 HOHH = HOL +
     9 
    10 consts
    11 
    12 (* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A		*)
    13   "Dand"	:: [bool, bool] => bool		(infixr ".." 28)
    14   ":-"		:: [bool, bool] => bool		(infixl 29)
    15 
    16 (* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G 
    17 			       | True | !x. G | D => G			*)
    18 (*","           :: [bool, bool] => bool		(infixr 35)*)
    19   "=>"		:: [bool, bool] => bool		(infixr 27)
    20 
    21 translations
    22 
    23   "D :- G"	=>	"G --> D"
    24   "D1 .. D2"	=>	"D1 & D2"
    25 (*"G1 , G2"	=>	"G1 & G2"*)
    26   "D => G"	=>	"D --> G"
    27 
    28 end
    29