equal
deleted
inserted
replaced
53 addcongs [if_weak_cong] |
53 addcongs [if_weak_cong] |
54 setSolver type_solver); |
54 setSolver type_solver); |
55 |
55 |
56 local |
56 local |
57 |
57 |
58 fun prove_bex_tac ss = unfold_tac ss [Bex_def] THEN Quantifier1.prove_one_point_ex_tac; |
58 val unfold_bex_tac = unfold_tac [Bex_def]; |
|
59 fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; |
59 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; |
60 val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; |
60 |
61 |
61 fun prove_ball_tac ss = unfold_tac ss [Ball_def] THEN Quantifier1.prove_one_point_all_tac; |
62 val unfold_ball_tac = unfold_tac [Ball_def]; |
|
63 fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; |
62 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; |
64 val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; |
63 |
65 |
64 in |
66 in |
65 |
67 |
66 val defBEX_regroup = Simplifier.simproc (the_context ()) |
68 val defBEX_regroup = Simplifier.simproc (the_context ()) |