equal
deleted
inserted
replaced
1203 by blast |
1203 by blast |
1204 |
1204 |
1205 use "Tools/simpdata.ML" |
1205 use "Tools/simpdata.ML" |
1206 ML {* open Simpdata *} |
1206 ML {* open Simpdata *} |
1207 |
1207 |
1208 setup {* Simplifier.map_simpset (K HOL_basic_ss) *} |
1208 setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *} |
1209 |
1209 |
1210 simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *} |
1210 simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *} |
1211 simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *} |
1211 simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *} |
1212 |
1212 |
1213 setup {* |
1213 setup {* |