adapted fact names;
authorwenzelm
Wed Jul 24 00:11:24 2002 +0200 (2002-07-24)
changeset 134130b60b9e18a26
parent 13412 666137b488a4
child 13414 15597d502035
adapted fact names;
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Wed Jul 24 00:10:52 2002 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Wed Jul 24 00:11:24 2002 +0200
     1.3 @@ -46,12 +46,12 @@
     1.4  val product_typeN = "Record.product_type";
     1.5  
     1.6  val product_typeI = thm "product_typeI";
     1.7 -val product_type_inject = thm "product_type_inject";
     1.8 -val product_type_conv1 = thm "product_type_conv1";
     1.9 -val product_type_conv2 = thm "product_type_conv2";
    1.10 -val product_type_induct = thm "product_type_induct";
    1.11 -val product_type_cases = thm "product_type_cases";
    1.12 -val product_type_split_paired_all = thm "product_type_split_paired_all";
    1.13 +val product_type_inject = thm "product_type.inject";
    1.14 +val product_type_conv1 = thm "product_type.conv1";
    1.15 +val product_type_conv2 = thm "product_type.conv2";
    1.16 +val product_type_induct = thm "product_type.induct";
    1.17 +val product_type_cases = thm "product_type.cases";
    1.18 +val product_type_split_paired_all = thm "product_type.split_paired_all";
    1.19  
    1.20  
    1.21  
     2.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Jul 24 00:10:52 2002 +0200
     2.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Jul 24 00:11:24 2002 +0200
     2.3 @@ -35,17 +35,16 @@
     2.4  (** theory context references **)
     2.5  
     2.6  val type_definitionN = "Typedef.type_definition";
     2.7 -val type_definition_def = thm "type_definition_def";
     2.8  
     2.9 -val Rep = thm "Rep";
    2.10 -val Rep_inverse = thm "Rep_inverse";
    2.11 -val Abs_inverse = thm "Abs_inverse";
    2.12 -val Rep_inject = thm "Rep_inject";
    2.13 -val Abs_inject = thm "Abs_inject";
    2.14 -val Rep_cases = thm "Rep_cases";
    2.15 -val Abs_cases = thm "Abs_cases";
    2.16 -val Rep_induct = thm "Rep_induct";
    2.17 -val Abs_induct = thm "Abs_induct";
    2.18 +val Rep = thm "type_definition.Rep";
    2.19 +val Rep_inverse = thm "type_definition.Rep_inverse";
    2.20 +val Abs_inverse = thm "type_definition.Abs_inverse";
    2.21 +val Rep_inject = thm "type_definition.Rep_inject";
    2.22 +val Abs_inject = thm "type_definition.Abs_inject";
    2.23 +val Rep_cases = thm "type_definition.Rep_cases";
    2.24 +val Abs_cases = thm "type_definition.Abs_cases";
    2.25 +val Rep_induct = thm "type_definition.Rep_induct";
    2.26 +val Abs_induct = thm "type_definition.Abs_induct";
    2.27  
    2.28  
    2.29