equal
deleted
inserted
replaced
305 handle THM _ => |
305 handle THM _ => |
306 forward_res make_nnf1 |
306 forward_res make_nnf1 |
307 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) |
307 (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) |
308 handle THM _ => th; |
308 handle THM _ => th; |
309 |
309 |
310 fun make_nnf th = make_nnf1 (check_no_bool th); |
310 (*The simplification removes occurrences of True and False.*) |
|
311 val nnf_ss = HOL_basic_ss addsimps Ball_def::Bex_def::simp_thms; |
|
312 |
|
313 fun make_nnf th = th |> simplify nnf_ss |
|
314 |> check_no_bool |> make_nnf1 |
311 |
315 |
312 (*Pull existential quantifiers (Skolemization)*) |
316 (*Pull existential quantifiers (Skolemization)*) |
313 fun skolemize th = |
317 fun skolemize th = |
314 if not (has_consts ["Ex"] (prop_of th)) then th |
318 if not (has_consts ["Ex"] (prop_of th)) then th |
315 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2, |
319 else (skolemize (tryres(th, [choice, conj_exD1, conj_exD2, |