--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 11 18:54:36 2014 +0200
@@ -706,13 +706,13 @@
text {*
\begin{matharray}{rcl}
@{command_def (HOL) "old_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def (HOL) "rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+ @{command_def (HOL) "old_rep_datatype"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
\end{matharray}
@{rail \<open>
@@{command (HOL) old_datatype} (spec + @'and')
;
- @@{command (HOL) rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
+ @@{command (HOL) old_rep_datatype} ('(' (@{syntax name} +) ')')? (@{syntax term} +)
;
spec: @{syntax typespec_sorts} @{syntax mixfix}? '=' (cons + '|')
@@ -725,7 +725,7 @@
\item @{command (HOL) "old_datatype"} defines old-style inductive
datatypes in HOL.
- \item @{command (HOL) "rep_datatype"} represents existing types as
+ \item @{command (HOL) "old_rep_datatype"} represents existing types as
old-style datatypes.
\end{description}
--- a/src/HOL/Code_Numeral.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Code_Numeral.thy Thu Sep 11 18:54:36 2014 +0200
@@ -800,7 +800,7 @@
declare Suc.rep_eq [simp]
-rep_datatype "0::natural" Suc
+old_rep_datatype "0::natural" Suc
by (transfer, fact nat.induct nat.inject nat.distinct)+
lemma natural_cases [case_names nat, cases type: natural]:
--- a/src/HOL/HOLCF/Lift.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/HOLCF/Lift.thy Thu Sep 11 18:54:36 2014 +0200
@@ -29,7 +29,7 @@
apply (simp add: Def_def)
done
-rep_datatype "\<bottom>\<Colon>'a lift" Def
+old_rep_datatype "\<bottom>\<Colon>'a lift" Def
by (erule lift_induct) (simp_all add: Def_def Abs_lift_inject inst_lift_pcpo)
text {* @{term bottom} and @{term Def} *}
--- a/src/HOL/Inductive.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Inductive.thy Thu Sep 11 18:54:36 2014 +0200
@@ -10,7 +10,7 @@
"inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
"monos" and
"print_inductives" :: diag and
- "rep_datatype" :: thy_goal and
+ "old_rep_datatype" :: thy_goal and
"primrec" :: thy_decl
begin
--- a/src/HOL/Library/Bit.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Library/Bit.thy Thu Sep 11 18:54:36 2014 +0200
@@ -27,7 +27,7 @@
end
-rep_datatype "0::bit" "1::bit"
+old_rep_datatype "0::bit" "1::bit"
proof -
fix P and x :: bit
assume "P (0::bit)" and "P (1::bit)"
--- a/src/HOL/Library/Extended_Nat.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Thu Sep 11 18:54:36 2014 +0200
@@ -44,7 +44,7 @@
by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject)
qed
-rep_datatype enat "\<infinity> :: enat"
+old_rep_datatype enat "\<infinity> :: enat"
proof -
fix P i assume "\<And>j. P (enat j)" "P \<infinity>"
then show "P i"
--- a/src/HOL/Nat.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Nat.thy Thu Sep 11 18:54:36 2014 +0200
@@ -96,10 +96,10 @@
apply (simp only: Suc_not_Zero)
done
--- {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+-- {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
setup {* Sign.mandatory_path "old" *}
-rep_datatype "0 \<Colon> nat" Suc
+old_rep_datatype "0 \<Colon> nat" Suc
apply (erule nat_induct0, assumption)
apply (rule nat.inject)
apply (rule nat.distinct(1))
--- a/src/HOL/Product_Type.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Product_Type.thy Thu Sep 11 18:54:36 2014 +0200
@@ -15,11 +15,11 @@
free_constructors case_bool for True | False
by auto
-text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
setup {* Sign.mandatory_path "old" *}
-rep_datatype True False by (auto intro: bool_induct)
+old_rep_datatype True False by (auto intro: bool_induct)
setup {* Sign.parent_path *}
@@ -84,11 +84,11 @@
free_constructors case_unit for "()"
by auto
-text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
setup {* Sign.mandatory_path "old" *}
-rep_datatype "()" by simp
+old_rep_datatype "()" by simp
setup {* Sign.parent_path *}
@@ -257,11 +257,11 @@
by (simp add: Pair_def Abs_prod_inject)
qed
-text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
setup {* Sign.mandatory_path "old" *}
-rep_datatype Pair
+old_rep_datatype Pair
by (erule prod_cases) (rule prod.inject)
setup {* Sign.parent_path *}
--- a/src/HOL/Sum_Type.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Sum_Type.thy Thu Sep 11 18:54:36 2014 +0200
@@ -90,11 +90,11 @@
| Inr projr
by (erule sumE, assumption) (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
-text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}
+text {* Avoid name clashes by prefixing the output of @{text old_rep_datatype} with @{text old}. *}
setup {* Sign.mandatory_path "old" *}
-rep_datatype Inl Inr
+old_rep_datatype Inl Inr
proof -
fix P
fix s :: "'a + 'b"
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Sep 11 18:54:36 2014 +0200
@@ -673,7 +673,8 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively"
+ Outer_Syntax.command @{command_spec "old_rep_datatype"}
+ "register existing types as old-style datatypes"
(Scan.repeat1 Parse.term >> (fn ts =>
Toplevel.theory_to_proof (rep_datatype_cmd Old_Datatype_Aux.default_config (K I) ts)));