equal
deleted
inserted
replaced
52 by (simp add: fequal_def) |
52 by (simp add: fequal_def) |
53 |
53 |
54 lemma equal_imp_fequal: "X=Y ==> fequal X Y" |
54 lemma equal_imp_fequal: "X=Y ==> fequal X Y" |
55 by (simp add: fequal_def) |
55 by (simp add: fequal_def) |
56 |
56 |
|
57 lemma COMBK1: "COMBK P == (%Q. P)" |
|
58 apply (rule eq_reflection) |
|
59 apply (rule ext) |
|
60 apply (simp add: COMBK_def) |
|
61 done |
|
62 |
|
63 lemma COMBI1: "COMBI == (%P. P)" |
|
64 apply (rule eq_reflection) |
|
65 apply (rule ext) |
|
66 apply (simp add: COMBI_def) |
|
67 done |
|
68 |
|
69 lemma COMBB1: "COMBB P Q == %R. P (Q R)" |
|
70 apply (rule eq_reflection) |
|
71 apply (rule ext) |
|
72 apply (simp add: COMBB_def) |
|
73 done |
|
74 |
|
75 |
57 use "Tools/res_axioms.ML" |
76 use "Tools/res_axioms.ML" |
58 use "Tools/res_hol_clause.ML" |
77 use "Tools/res_hol_clause.ML" |
59 use "Tools/res_atp.ML" |
78 use "Tools/res_atp.ML" |
60 use "Tools/reconstruction.ML" |
79 use "Tools/reconstruction.ML" |
61 |
80 |