equal
deleted
inserted
replaced
1259 |
1259 |
1260 ML_file "Tools/set_comprehension_pointfree.ML" |
1260 ML_file "Tools/set_comprehension_pointfree.ML" |
1261 |
1261 |
1262 setup \<open> |
1262 setup \<open> |
1263 Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs |
1263 Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs |
1264 [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}], |
1264 [Simplifier.make_simproc @{context} "set comprehension" |
1265 proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}]) |
1265 {lhss = [@{term "Collect P"}], |
|
1266 proc = K Set_Comprehension_Pointfree.code_simproc, |
|
1267 identifier = []}]) |
1266 \<close> |
1268 \<close> |
1267 |
1269 |
1268 |
1270 |
1269 subsection \<open>Inductively defined sets\<close> |
1271 subsection \<open>Inductively defined sets\<close> |
1270 |
1272 |