src/ZF/OrdQuant.thy
 changeset 18324 d1c4b1112e33 parent 17876 b9c92f384109 child 24893 b8ef7afe3a6b
equal inserted replaced
18323:4365c8d84f69 18324:d1c4b1112e33
`   398 text {* Setting up the one-point-rule simproc *}`
`   398 text {* Setting up the one-point-rule simproc *}`
`   399 `
`   399 `
`   400 ML_setup {*`
`   400 ML_setup {*`
`   401 local`
`   401 local`
`   402 `
`   402 `
`   403 fun prove_rex_tac ss = unfold_tac ss [rex_def] THEN Quantifier1.prove_one_point_ex_tac;`
`   403 val unfold_rex_tac = unfold_tac [rex_def];`
`       `
`   404 fun prove_rex_tac ss = unfold_rex_tac ss THEN Quantifier1.prove_one_point_ex_tac;`
`   404 val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;`
`   405 val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;`
`   405 `
`   406 `
`   406 fun prove_rall_tac ss = unfold_tac ss [rall_def] THEN Quantifier1.prove_one_point_all_tac;`
`   407 val unfold_rall_tac = unfold_tac [rall_def];`
`       `
`   408 fun prove_rall_tac ss = unfold_rall_tac ss THEN Quantifier1.prove_one_point_all_tac;`
`   407 val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;`
`   409 val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;`
`   408 `
`   410 `
`   409 in`
`   411 in`
`   410 `
`   412 `
`   411 val defREX_regroup = Simplifier.simproc (the_context ())`
`   413 val defREX_regroup = Simplifier.simproc (the_context ())`