ignore morphism more explicitly;
authorwenzelm
Mon Jun 25 15:14:07 2012 +0200 (2012-06-25)
changeset 4812487c831e30f0a
parent 48121 fa7c0c659798
child 48125 602dc0215954
ignore morphism more explicitly;
tuned headers;
CONTRIBUTORS
src/HOL/Finite_Set.thy
src/HOL/Tools/set_comprehension_pointfree.ML
     1.1 --- a/CONTRIBUTORS	Mon Jun 25 14:21:32 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Mon Jun 25 15:14:07 2012 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA
     1.5    Simproc for rewriting set comprehensions into pointfree expressions
     1.6  
     1.7 +
     1.8  Contributions to Isabelle2012
     1.9  -----------------------------
    1.10  
     2.1 --- a/src/HOL/Finite_Set.thy	Mon Jun 25 14:21:32 2012 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Mon Jun 25 15:14:07 2012 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4  use "Tools/set_comprehension_pointfree.ML"
     2.5  
     2.6  simproc_setup finite_Collect ("finite (Collect P)") =
     2.7 -  {* Set_Comprehension_Pointfree.simproc *}
     2.8 +  {* K Set_Comprehension_Pointfree.simproc *}
     2.9  
    2.10  
    2.11  lemma finite_induct [case_names empty insert, induct set: finite]:
     3.1 --- a/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 14:21:32 2012 +0200
     3.2 +++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Mon Jun 25 15:14:07 2012 +0200
     3.3 @@ -1,13 +1,13 @@
     3.4 -(*  Title:      HOL/ex/set_comprehension_pointfree.ML
     3.5 +(*  Title:      HOL/Tools/set_comprehension_pointfree.ML
     3.6      Author:     Felix Kuperjans, Lukas Bulwahn, TU Muenchen
     3.7 -                Rafal Kolanski, NICTA
     3.8 +    Author:     Rafal Kolanski, NICTA
     3.9  
    3.10  Simproc for rewriting set comprehensions to pointfree expressions.
    3.11  *)
    3.12  
    3.13  signature SET_COMPREHENSION_POINTFREE =
    3.14  sig
    3.15 -  val simproc : morphism -> simpset -> cterm -> thm option
    3.16 +  val simproc : simpset -> cterm -> thm option
    3.17    val rewrite_term : term -> term option
    3.18    val conv : Proof.context -> term -> thm option
    3.19  end
    3.20 @@ -141,7 +141,7 @@
    3.21  
    3.22  (* simproc *)
    3.23  
    3.24 -fun simproc _ ss redex =
    3.25 +fun simproc ss redex =
    3.26    let
    3.27      val ctxt = Simplifier.the_context ss
    3.28      val _ $ set_compr = term_of redex