centralized enriched_type declaration, thanks to in-situ available Isar commands
authorhaftmann
Sun Apr 15 20:51:07 2012 +0200 (2012-04-15)
changeset 47488be6dd389639d
parent 47487 54a2f155621b
child 47489 04e7d09ade7a
centralized enriched_type declaration, thanks to in-situ available Isar commands
src/HOL/Datatype.thy
src/HOL/Fun.thy
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Datatype.thy	Sun Apr 15 20:41:46 2012 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Sun Apr 15 20:51:07 2012 +0200
     1.3 @@ -14,12 +14,6 @@
     1.4    ("Tools/Datatype/datatype_realizer.ML")
     1.5  begin
     1.6  
     1.7 -subsection {* Prelude: lifting over function space *}
     1.8 -
     1.9 -enriched_type map_fun: map_fun
    1.10 -  by (simp_all add: fun_eq_iff)
    1.11 -
    1.12 -
    1.13  subsection {* The datatype universe *}
    1.14  
    1.15  definition "Node = {p. EX f x k. p = (f :: nat => 'b + nat, x ::'a + nat) & f k = Inr 0}"
    1.16 @@ -532,3 +526,4 @@
    1.17  setup Datatype_Realizer.setup
    1.18  
    1.19  end
    1.20 +
     2.1 --- a/src/HOL/Fun.thy	Sun Apr 15 20:41:46 2012 +0200
     2.2 +++ b/src/HOL/Fun.thy	Sun Apr 15 20:51:07 2012 +0200
     2.3 @@ -803,4 +803,11 @@
     2.4  
     2.5  use "Tools/enriched_type.ML"
     2.6  
     2.7 +enriched_type map_fun: map_fun
     2.8 +  by (simp_all add: fun_eq_iff)
     2.9 +
    2.10 +enriched_type vimage
    2.11 +  by (simp_all add: fun_eq_iff vimage_compose)
    2.12 +
    2.13  end
    2.14 +
     3.1 --- a/src/HOL/Quotient.thy	Sun Apr 15 20:41:46 2012 +0200
     3.2 +++ b/src/HOL/Quotient.thy	Sun Apr 15 20:51:07 2012 +0200
     3.3 @@ -19,13 +19,6 @@
     3.4  begin
     3.5  
     3.6  text {*
     3.7 -  An aside: contravariant functorial structure of sets.
     3.8 -*}
     3.9 -
    3.10 -enriched_type vimage
    3.11 -  by (simp_all add: fun_eq_iff vimage_compose)
    3.12 -
    3.13 -text {*
    3.14    Basic definition for equivalence relations
    3.15    that are represented by predicates.
    3.16  *}
    3.17 @@ -911,3 +904,4 @@
    3.18    fun_rel (infixr "===>" 55)
    3.19  
    3.20  end
    3.21 +