--- a/src/HOL/ex/Records.thy Mon Jul 26 14:44:07 2010 +0200
+++ b/src/HOL/ex/Records.thy Tue Jul 27 17:09:35 2010 +0200
@@ -249,8 +249,8 @@
text {* In some cases its convenient to automatically split
(quantified) records. For this purpose there is the simproc @{ML [source]
-"Record.record_split_simproc"} and the tactic @{ML [source]
-"Record.record_split_simp_tac"}. The simplification procedure
+"Record.split_simproc"} and the tactic @{ML [source]
+"Record.split_simp_tac"}. The simplification procedure
only splits the records, whereas the tactic also simplifies the
resulting goal with the standard record simplification rules. A
(generalized) predicate on the record is passed as parameter that
@@ -259,51 +259,51 @@
the quantifier). The value @{ML "0"} indicates no split, a value
greater @{ML "0"} splits up to the given bound of record extension and
finally the value @{ML "~1"} completely splits the record.
-@{ML [source] "Record.record_split_simp_tac"} additionally takes a list of
+@{ML [source] "Record.split_simp_tac"} additionally takes a list of
equations for simplification and can also split fixed record variables.
*}
lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
+ (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
apply simp
done
lemma "(\<forall>r. P (xpos r)) \<longrightarrow> (\<forall>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
apply simp
done
lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
+ (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
apply simp
done
lemma "(\<exists>r. P (xpos r)) \<longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
apply simp
done
lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
+ (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
apply auto
done
lemma "\<And>r. P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
apply auto
done
lemma "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
apply auto
done
lemma fixes r shows "P (xpos r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
apply auto
done
@@ -316,7 +316,7 @@
have "\<exists>x. P x"
using pre
apply -
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
apply auto
done
}
@@ -324,13 +324,13 @@
qed
text {* The effect of simproc @{ML [source]
-"Record.record_ex_sel_eq_simproc"} is illustrated by the
+"Record.ex_sel_eq_simproc"} is illustrated by the
following lemma.
*}
lemma "\<exists>r. xpos r = x"
apply (tactic {*simp_tac
- (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*})
+ (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*})
done