--- a/CONTRIBUTORS Mon Jun 25 14:21:32 2012 +0200
+++ b/CONTRIBUTORS Mon Jun 25 15:14:07 2012 +0200
@@ -9,6 +9,7 @@
* June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
Simproc for rewriting set comprehensions into pointfree expressions
+
Contributions to Isabelle2012
-----------------------------
--- a/src/HOL/Finite_Set.thy Mon Jun 25 14:21:32 2012 +0200
+++ b/src/HOL/Finite_Set.thy Mon Jun 25 15:14:07 2012 +0200
@@ -20,7 +20,7 @@
use "Tools/set_comprehension_pointfree.ML"
simproc_setup finite_Collect ("finite (Collect P)") =
- {* Set_Comprehension_Pointfree.simproc *}
+ {* K Set_Comprehension_Pointfree.simproc *}
lemma finite_induct [case_names empty insert, induct set: finite]:
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Mon Jun 25 14:21:32 2012 +0200
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Mon Jun 25 15:14:07 2012 +0200
@@ -1,13 +1,13 @@
-(* Title: HOL/ex/set_comprehension_pointfree.ML
+(* Title: HOL/Tools/set_comprehension_pointfree.ML
Author: Felix Kuperjans, Lukas Bulwahn, TU Muenchen
- Rafal Kolanski, NICTA
+ Author: Rafal Kolanski, NICTA
Simproc for rewriting set comprehensions to pointfree expressions.
*)
signature SET_COMPREHENSION_POINTFREE =
sig
- val simproc : morphism -> simpset -> cterm -> thm option
+ val simproc : simpset -> cterm -> thm option
val rewrite_term : term -> term option
val conv : Proof.context -> term -> thm option
end
@@ -141,7 +141,7 @@
(* simproc *)
-fun simproc _ ss redex =
+fun simproc ss redex =
let
val ctxt = Simplifier.the_context ss
val _ $ set_compr = term_of redex