theorems foo.splits = foo.split foo.split_asm;
authorwenzelm
Tue Jul 18 21:09:18 2000 +0200 (2000-07-18)
changeset 93868800603d99f6
parent 9385 6e1ac1629ac7
child 9387 3bab31b55a95
theorems foo.splits = foo.split foo.split_asm;
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jul 18 21:08:57 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jul 18 21:09:18 2000 +0200
     1.3 @@ -559,6 +559,7 @@
     1.4            nchotomys ~~ case_congs);
     1.5  
     1.6      val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
     1.7 +    val split_thms = split ~~ split_asm;
     1.8  
     1.9      val thy12 = thy11 |>
    1.10        Theory.add_path (space_implode "_" new_type_names) |>
    1.11 @@ -568,8 +569,8 @@
    1.12          (("", weak_case_congs), [cong_add_global])]) |>
    1.13        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.14        add_cases_induct dt_infos |>
    1.15 -      Theory.parent_path;
    1.16 -
    1.17 +      Theory.parent_path |>
    1.18 +      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
    1.19    in
    1.20      (thy12,
    1.21       {distinct = distinct,
    1.22 @@ -577,7 +578,7 @@
    1.23        exhaustion = exhaustion,
    1.24        rec_thms = rec_thms,
    1.25        case_thms = case_thms,
    1.26 -      split_thms = split ~~ split_asm,
    1.27 +      split_thms = split_thms,
    1.28        induction = induct,
    1.29        size = size_thms,
    1.30        simps = simps})
    1.31 @@ -626,8 +627,8 @@
    1.32          (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
    1.33        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.34        add_cases_induct dt_infos |>
    1.35 -      Theory.parent_path;
    1.36 -
    1.37 +      Theory.parent_path |>
    1.38 +      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
    1.39    in
    1.40      (thy12,
    1.41       {distinct = distinct,
    1.42 @@ -732,7 +733,8 @@
    1.43          (("", weak_case_congs), [Simplifier.change_global_ss (op addcongs)])]) |>
    1.44        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.45        add_cases_induct dt_infos |>
    1.46 -      Theory.parent_path;
    1.47 +      Theory.parent_path |>
    1.48 +      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
    1.49    in
    1.50      (thy11,
    1.51       {distinct = distinct,