src/HOL/Tools/typedef_package.ML
changeset 13413 0b60b9e18a26
parent 12876 a70df1e5bf10
child 13443 1c3327c348b3
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Jul 24 00:10:52 2002 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Jul 24 00:11:24 2002 +0200
     1.3 @@ -35,17 +35,16 @@
     1.4  (** theory context references **)
     1.5  
     1.6  val type_definitionN = "Typedef.type_definition";
     1.7 -val type_definition_def = thm "type_definition_def";
     1.8  
     1.9 -val Rep = thm "Rep";
    1.10 -val Rep_inverse = thm "Rep_inverse";
    1.11 -val Abs_inverse = thm "Abs_inverse";
    1.12 -val Rep_inject = thm "Rep_inject";
    1.13 -val Abs_inject = thm "Abs_inject";
    1.14 -val Rep_cases = thm "Rep_cases";
    1.15 -val Abs_cases = thm "Abs_cases";
    1.16 -val Rep_induct = thm "Rep_induct";
    1.17 -val Abs_induct = thm "Abs_induct";
    1.18 +val Rep = thm "type_definition.Rep";
    1.19 +val Rep_inverse = thm "type_definition.Rep_inverse";
    1.20 +val Abs_inverse = thm "type_definition.Abs_inverse";
    1.21 +val Rep_inject = thm "type_definition.Rep_inject";
    1.22 +val Abs_inject = thm "type_definition.Abs_inject";
    1.23 +val Rep_cases = thm "type_definition.Rep_cases";
    1.24 +val Abs_cases = thm "type_definition.Abs_cases";
    1.25 +val Rep_induct = thm "type_definition.Rep_induct";
    1.26 +val Abs_induct = thm "type_definition.Abs_induct";
    1.27  
    1.28  
    1.29