equal
deleted
inserted
replaced
71 val counter = Unsynchronized.ref 0; |
71 val counter = Unsynchronized.ref 0; |
72 |
72 |
73 val resolution_thm = |
73 val resolution_thm = |
74 @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} |
74 @{lemma "(P ==> False) ==> (~ P ==> False) ==> False" by (rule case_split)} |
75 |
75 |
76 val cP = Thm.cterm_of @{theory} (Var (("P", 0), HOLogic.boolT)); |
76 val cP = Thm.global_cterm_of @{theory} (Var (("P", 0), HOLogic.boolT)); |
77 |
77 |
78 (* ------------------------------------------------------------------------- *) |
78 (* ------------------------------------------------------------------------- *) |
79 (* lit_ord: an order on integers that considers their absolute values only, *) |
79 (* lit_ord: an order on integers that considers their absolute values only, *) |
80 (* thereby treating integers that represent the same atom (positively *) |
80 (* thereby treating integers that represent the same atom (positively *) |
81 (* or negatively) as equal *) |
81 (* or negatively) as equal *) |