# HG changeset patch
# User wenzelm
# Date 1404240445 -7200
# Node ID 08e5c7bc515a5140b3a5eef2348596180d143955
# Parent  fa14d60a8cca6ba6c70327d71c2d943cb43907d2
tuned;

diff -r fa14d60a8cca -r 08e5c7bc515a src/Doc/Isar_Ref/Quick_Reference.thy
--- a/src/Doc/Isar_Ref/Quick_Reference.thy	Tue Jul 01 20:43:51 2014 +0200
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Tue Jul 01 20:47:25 2014 +0200
@@ -98,7 +98,8 @@
 
 text {*
   \begin{tabular}{ll}
-    @{command "print_state"} & print current state \\
+    @{command "print_state"} & print proof state \\
+    @{command "print_statement"} & print fact in long statement form \\
     @{command "thm"}~@{text a} & print fact \\
     @{command "prop"}~@{text \<phi>} & print proposition \\
     @{command "term"}~@{text t} & print term \\