src/HOL/Prolog/HOHH.thy
changeset 21425 c11ab38b78a7
parent 17311 5b1d47d920ce
child 21588 cd0dc678a205
     1.1 --- a/src/HOL/Prolog/HOHH.thy	Mon Nov 20 11:51:10 2006 +0100
     1.2 +++ b/src/HOL/Prolog/HOHH.thy	Mon Nov 20 21:23:12 2006 +0100
     1.3 @@ -7,18 +7,27 @@
     1.4  
     1.5  theory HOHH
     1.6  imports HOL
     1.7 +uses "prolog.ML"
     1.8  begin
     1.9  
    1.10 +method_setup ptac =
    1.11 +  {* Method.thms_args (Method.SIMPLE_METHOD' HEADGOAL o Prolog.ptac) *}
    1.12 +  "Basic Lambda Prolog interpreter"
    1.13 +
    1.14 +method_setup prolog =
    1.15 +  {* Method.thms_args (Method.SIMPLE_METHOD o Prolog.prolog_tac) *}
    1.16 +  "Lambda Prolog interpreter"
    1.17 +
    1.18  consts
    1.19  
    1.20  (* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
    1.21 -  "Dand"        :: "[bool, bool] => bool"         (infixr ".." 28)
    1.22 -  ":-"          :: "[bool, bool] => bool"         (infixl 29)
    1.23 +  Dand        :: "[bool, bool] => bool"         (infixr ".." 28)
    1.24 +  Dif        :: "[bool, bool] => bool"         (infixl ":-" 29)
    1.25  
    1.26  (* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
    1.27                                 | True | !x. G | D => G                  *)
    1.28 -(*","           :: "[bool, bool] => bool"         (infixr 35)*)
    1.29 -  "=>"          :: "[bool, bool] => bool"         (infixr 27)
    1.30 +(*Dand'         :: "[bool, bool] => bool"         (infixr "," 35)*)
    1.31 +  Dimp          :: "[bool, bool] => bool"         (infixr "=>" 27)
    1.32  
    1.33  translations
    1.34