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
oheimb@9015
     1
(* higher-order hereditary Harrop formulas *)
oheimb@9015
     2
oheimb@9015
     3
HOHH = HOL +
oheimb@9015
     4
oheimb@9015
     5
consts
oheimb@9015
     6
oheimb@9015
     7
(* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A		*)
oheimb@9015
     8
  "Dand"	:: [bool, bool] => bool		(infixr ".." 28)
oheimb@9015
     9
  ":-"		:: [bool, bool] => bool		(infixl 29)
oheimb@9015
    10
oheimb@9015
    11
(* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G 
oheimb@9015
    12
			       | True | !x. G | D => G			*)
oheimb@9015
    13
(*","           :: [bool, bool] => bool		(infixr 35)*)
oheimb@9015
    14
  "=>"		:: [bool, bool] => bool		(infixr 27)
oheimb@9015
    15
oheimb@9015
    16
translations
oheimb@9015
    17
oheimb@9015
    18
  "D :- G"	=>	"G --> D"
oheimb@9015
    19
  "D1 .. D2"	=>	"D1 & D2"
oheimb@9015
    20
(*"G1 , G2"	=>	"G1 & G2"*)
oheimb@9015
    21
  "D => G"	=>	"D --> G"
oheimb@9015
    22
oheimb@9015
    23
end
oheimb@9015
    24