src/HOL/ex/Records.thy

 lemma "r (| xpos := x, ypos := y, xpos := x' |) = r (| ypos := y, xpos := x' |)"
   by simp
 
 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
 decides whether or how `deep' to split the record. It can peek on the
 subterm starting at the quantified occurrence of the record (including
 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
 
 
 lemma True

     fix P r
     assume pre: "P (xpos r)"
     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
   }
   show ?thesis ..
 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
 
 
 subsection {* A more complex record expression *}