Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Prolog/HOHH.thy
author oheimb
Fri, 02 Jun 2000 12:44:04 +0200
changeset 9015 8006e9009621
child 13208 965f95a3abd9
permissions -rw-r--r--
added HOL/Prolog

(* 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
isabelle