# HG changeset patch
# User kleing
# Date 1452486552 28800
# Node ID 13f0fa687aa760fd8b71f9c579d4f6af502398f0
# Parent  b8c973d90ae7f3e970259ca2c6225ff06fb3ccac
isar-ref entry for print_record

diff -r b8c973d90ae7 -r 13f0fa687aa7 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Jan 10 20:13:29 2016 -0800
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Jan 10 20:29:12 2016 -0800
@@ -885,6 +885,7 @@
 text \<open>
   \begin{matharray}{rcl}
     @{command_def (HOL) "record"} & : & \<open>theory \<rightarrow> theory\<close> \\
+    @{command_def (HOL) "print_record"} & : & \<open>context \<rightarrow>\<close> \\
   \end{matharray}
 
   @{rail \<open>
@@ -892,6 +893,10 @@
       (@{syntax type} '+')? (constdecl +)
     ;
     constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}?
+    ;
+    @@{command (HOL) print_record} modes? @{syntax typespec_sorts}
+    ;
+    modes: '(' (@{syntax name} +) ')'
   \<close>}
 
   \<^descr> @{command (HOL) "record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t = \<tau> + c\<^sub>1 :: \<sigma>\<^sub>1
@@ -918,6 +923,10 @@
   \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n\<rparr>\<close>, likewise is \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m, \<zeta>) t_scheme\<close> made an abbreviation for
   \<open>\<lparr>c\<^sub>1 :: \<sigma>\<^sub>1, \<dots>, c\<^sub>n :: \<sigma>\<^sub>n, \<dots> ::
   \<zeta>\<rparr>\<close>.
+
+ \<^descr> @{command (HOL) "print_record"}~\<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close> prints the definition
+ of record \<open>(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>m) t\<close>. Optionally \<open>modes\<close> can be specified, which are
+ appended to the current print mode; see \secref{sec:print-modes}.
 \<close>