src/Sequents/ILL/ILL_predlog.thy
changeset 17481 75166ebb619b
parent 14854 61bdf2ae4dc5
     1.1 --- a/src/Sequents/ILL/ILL_predlog.thy	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/ILL/ILL_predlog.thy	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,36 +1,32 @@
     1.4 -(* 
     1.5 -    File:	 /Nfs/toton/usr20/sk/isa_files/ll/NEW/pred_log.thy
     1.6 -    Theory Name: pred_log
     1.7 -    Logic Image: HOL
     1.8 -*)
     1.9 +(* $Id$ *)
    1.10  
    1.11 -ILL_predlog  =  ILL +
    1.12 +theory ILL_predlog
    1.13 +imports ILL
    1.14 +begin
    1.15  
    1.16 -types
    1.17 -    plf
    1.18 -    
    1.19 +typedecl plf
    1.20 +
    1.21  consts
    1.22 -
    1.23    "&"   :: "[plf,plf] => plf"   (infixr 35)
    1.24    "|"   :: "[plf,plf] => plf"   (infixr 35)
    1.25    ">"   :: "[plf,plf] => plf"   (infixr 35)
    1.26    "="   :: "[plf,plf] => plf"   (infixr 35)
    1.27    "@NG" :: "plf => plf"   ("- _ " [50] 55)
    1.28    ff    :: "plf"
    1.29 -  
    1.30 +
    1.31    PL    :: "plf => o"      ("[* / _ / *]" [] 100)
    1.32  
    1.33  
    1.34  translations
    1.35  
    1.36 -  "[* A & B *]" == "[*A*] && [*B*]" 
    1.37 +  "[* A & B *]" == "[*A*] && [*B*]"
    1.38    "[* A | B *]" == "![*A*] ++ ![*B*]"
    1.39    "[* - A *]"   == "[*A > ff*]"
    1.40    "[* ff *]"    == "0"
    1.41    "[* A = B *]" => "[* (A > B) & (B > A) *]"
    1.42 -  
    1.43 +
    1.44    "[* A > B *]" == "![*A*] -o [*B*]"
    1.45 -  
    1.46 +
    1.47  (* another translations for linear implication:
    1.48    "[* A > B *]" == "!([*A*] -o [*B*])" *)
    1.49