equal
deleted
inserted
replaced
1 (* Title: LK/LK 
1 (* Title: LK/LK.ML 
2 ID: $Id$ 
2 ID: $Id$ 
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
4 Copyright 1993 University of Cambridge 
4 Copyright 1993 University of Cambridge 
5 
5 
6 Axiom to express monotonicity (a variant of the deduction theorem). Makes the 
6 Axiom to express monotonicity (a variant of the deduction theorem). Makes the 
11 
11 
12 CANNOT be added to LK0.thy because modal logic is built upon it, and 
12 CANNOT be added to LK0.thy because modal logic is built upon it, and 
13 various modal rules would become inconsistent. 
13 various modal rules would become inconsistent. 
14 *) 
14 *) 
15 
15 
16 LK = LK0 + 
16 theory LK 

17 imports LK0 

18 uses ("simpdata.ML") 

19 begin 
17 
20 
18 rules 
21 axioms 
19 
22 
20 monotonic "($H  P ==> $H  Q) ==> $H, P  Q" 
23 monotonic: "($H  P ==> $H  Q) ==> $H, P  Q" 
21 
24 
22 left_cong "[ P == P';  P' ==> ($H  $F) == ($H'  $F') ] 
25 left_cong: "[ P == P';  P' ==> ($H  $F) == ($H'  $F') ] 
23 ==> (P, $H  $F) == (P', $H'  $F')" 
26 ==> (P, $H  $F) == (P', $H'  $F')" 

27 

28 ML {* use_legacy_bindings (the_context ()) *} 

29 

30 use "simpdata.ML" 

31 
24 end 
32 end 