src/HOL/Product_Type.thy
changeset 58306 117ba6cbe414
parent 58292 e7320cceda9c
child 58389 ee1f45ca0d73
     1.1 --- a/src/HOL/Product_Type.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -15,11 +15,11 @@
     1.4  free_constructors case_bool for True | False
     1.5    by auto
     1.6  
     1.7 -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
     1.8 +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
     1.9  
    1.10  setup {* Sign.mandatory_path "old" *}
    1.11  
    1.12 -rep_datatype True False by (auto intro: bool_induct)
    1.13 +old_rep_datatype True False by (auto intro: bool_induct)
    1.14  
    1.15  setup {* Sign.parent_path *}
    1.16  
    1.17 @@ -84,11 +84,11 @@
    1.18  free_constructors case_unit for "()"
    1.19    by auto
    1.20  
    1.21 -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    1.22 +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
    1.23  
    1.24  setup {* Sign.mandatory_path "old" *}
    1.25  
    1.26 -rep_datatype "()" by simp
    1.27 +old_rep_datatype "()" by simp
    1.28  
    1.29  setup {* Sign.parent_path *}
    1.30  
    1.31 @@ -257,11 +257,11 @@
    1.32      by (simp add: Pair_def Abs_prod_inject)
    1.33  qed
    1.34  
    1.35 -text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
    1.36 +text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
    1.37  
    1.38  setup {* Sign.mandatory_path "old" *}
    1.39  
    1.40 -rep_datatype Pair
    1.41 +old_rep_datatype Pair
    1.42  by (erule prod_cases) (rule prod.inject)
    1.43  
    1.44  setup {* Sign.parent_path *}