src/HOL/ex/Records.thy

--- 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