# HG changeset patch
# User wenzelm
# Date 1289744701 -3600
# Node ID 270f47a6d8f81343c57ca2cced5f9a6aa5df82d6
# Parent  732f0826f1ba088769753f567be34465f68ef24f
tuned;

diff -r 732f0826f1ba -r 270f47a6d8f8 doc-src/IsarRef/Thy/Quick_Reference.thy
--- a/doc-src/IsarRef/Thy/Quick_Reference.thy	Sun Nov 14 15:21:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/Quick_Reference.thy	Sun Nov 14 15:25:01 2010 +0100
@@ -100,9 +100,9 @@
   \begin{tabular}{ll}
     @{command "pr"} & print current state \\
     @{command "thm"}~@{text a} & print fact \\
+    @{command "prop"}~@{text \<phi>} & print proposition \\
     @{command "term"}~@{text t} & print term \\
-    @{command "prop"}~@{text \<phi>} & print meta-level proposition \\
-    @{command "typ"}~@{text \<tau>} & print meta-level type \\
+    @{command "typ"}~@{text \<tau>} & print type \\
   \end{tabular}
 *}
 
diff -r 732f0826f1ba -r 270f47a6d8f8 doc-src/IsarRef/Thy/document/Quick_Reference.tex
--- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Sun Nov 14 15:21:49 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Sun Nov 14 15:25:01 2010 +0100
@@ -128,9 +128,9 @@
 \begin{tabular}{ll}
     \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}} & print current state \\
     \hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{a} & print fact \\
+    \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} & print proposition \\
     \hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} & print term \\
-    \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isaliteral{5C3C7068693E}{\isasymphi}}} & print meta-level proposition \\
-    \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} & print meta-level type \\
+    \hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} & print type \\
   \end{tabular}%
 \end{isamarkuptext}%
 \isamarkuptrue%