33 |
33 |
34 val lam_bb = get_axiom Lomega_thy "lam_bb"; |
34 val lam_bb = get_axiom Lomega_thy "lam_bb"; |
35 val pi_bb = get_axiom Lomega_thy "pi_bb"; |
35 val pi_bb = get_axiom Lomega_thy "pi_bb"; |
36 val Lomega = simple @ [lam_bb,pi_bb]; |
36 val Lomega = simple @ [lam_bb,pi_bb]; |
37 |
37 |
38 val LOmega_thy = merge_theories(L2_thy,Lomega_thy); |
38 val LOmega_thy = merge_theories "LOmega" (L2_thy,Lomega_thy); |
39 val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb]; |
39 val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb]; |
40 |
40 |
41 val LP_thy = |
41 val LP_thy = |
42 Cube.thy |
42 Cube.thy |
43 |> Theory.add_axioms |
43 |> Theory.add_axioms |
48 |
48 |
49 val lam_sb = get_axiom LP_thy "lam_sb"; |
49 val lam_sb = get_axiom LP_thy "lam_sb"; |
50 val pi_sb = get_axiom LP_thy "pi_sb"; |
50 val pi_sb = get_axiom LP_thy "pi_sb"; |
51 val LP = simple @ [lam_sb,pi_sb]; |
51 val LP = simple @ [lam_sb,pi_sb]; |
52 |
52 |
53 val LP2_thy = merge_theories(L2_thy,LP_thy); |
53 val LP2_thy = merge_theories "LP2" (L2_thy,LP_thy); |
54 val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb]; |
54 val LP2 = simple @ [lam_bs,pi_bs,lam_sb,pi_sb]; |
55 |
55 |
56 val LPomega_thy = merge_theories(LP_thy,Lomega_thy); |
56 val LPomega_thy = merge_theories "LPomega" (LP_thy,Lomega_thy); |
57 val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb]; |
57 val LPomega = simple @ [lam_bb,pi_bb,lam_sb,pi_sb]; |
58 |
58 |
59 val CC_thy = merge_theories(L2_thy,LPomega_thy); |
59 val CC_thy = merge_theories "CC" (L2_thy,LPomega_thy); |
60 val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb]; |
60 val CC = simple @ [lam_bs,pi_bs,lam_bb,pi_bb,lam_sb,pi_sb]; |