equal
deleted
inserted
replaced
33 val read_prop = certify o Simple_Syntax.read_prop; |
33 val read_prop = certify o Simple_Syntax.read_prop; |
34 |
34 |
35 val true_prop = certify Logic.true_prop; |
35 val true_prop = certify Logic.true_prop; |
36 val conjunction = certify Logic.conjunction; |
36 val conjunction = certify Logic.conjunction; |
37 |
37 |
38 fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B; |
38 fun mk_conjunction (A, B) = Thm.apply (Thm.apply conjunction A) B; |
39 |
39 |
40 fun mk_conjunction_balanced [] = true_prop |
40 fun mk_conjunction_balanced [] = true_prop |
41 | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts; |
41 | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts; |
42 |
42 |
43 fun dest_conjunction ct = |
43 fun dest_conjunction ct = |