17481

1 
(* $Id$ *)

6252

2 

17481

3 
theory ILL_predlog


4 
imports ILL


5 
begin

6252

6 

17481

7 
typedecl plf


8 

6252

9 
consts


10 
"&" :: "[plf,plf] => plf" (infixr 35)


11 
"" :: "[plf,plf] => plf" (infixr 35)


12 
">" :: "[plf,plf] => plf" (infixr 35)


13 
"=" :: "[plf,plf] => plf" (infixr 35)


14 
"@NG" :: "plf => plf" (" _ " [50] 55)


15 
ff :: "plf"

17481

16 

6252

17 
PL :: "plf => o" ("[* / _ / *]" [] 100)


18 


19 


20 
translations


21 

17481

22 
"[* A & B *]" == "[*A*] && [*B*]"

6252

23 
"[* A  B *]" == "![*A*] ++ ![*B*]"


24 
"[*  A *]" == "[*A > ff*]"


25 
"[* ff *]" == "0"


26 
"[* A = B *]" => "[* (A > B) & (B > A) *]"

17481

27 

6252

28 
"[* A > B *]" == "![*A*] o [*B*]"

17481

29 

6252

30 
(* another translations for linear implication:


31 
"[* A > B *]" == "!([*A*] o [*B*])" *)


32 


33 
end
