# HG changeset patch
# User wenzelm
# Date 1209814571 -7200
# Node ID de781c5c48c162ccc3bcd78d0fef918d61ec502e
# Parent  35809287ab231e75b44634c715701178c8b106e3
tuned syntax: props and facts;

diff -r 35809287ab23 -r de781c5c48c1 doc-src/IsarRef/Thy/Quick_Reference.thy
--- a/doc-src/IsarRef/Thy/Quick_Reference.thy	Sat May 03 13:26:08 2008 +0200
+++ b/doc-src/IsarRef/Thy/Quick_Reference.thy	Sat May 03 13:36:11 2008 +0200
@@ -27,21 +27,21 @@
   \end{tabular}
 
   \begin{matharray}{rcl}
-    @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: prop proof"} \Or @{command "definition"}~\dots \Or \dots \\[1ex]
+    @{text "theory\<dash>stmt"} & = & @{command "theorem"}~@{text "name: props proof"} \Or @{command "definition"}~\dots \Or \dots \\[1ex]
     @{text "proof"} & = & @{text "prfx\<^sup>*"}~@{command "proof"}~@{text "method stmt\<^sup>*"}~@{command "qed"}~@{text method} \\
     & \Or & @{text "prfx\<^sup>*"}~@{command "done"} \\[1ex]
     @{text prfx} & = & @{command "apply"}~@{text method} \\
-    & \Or & @{command "using"}~@{text "name\<^sup>+"} \\
-    & \Or & @{command "unfolding"}~@{text "name\<^sup>+"} \\
+    & \Or & @{command "using"}~@{text "facts"} \\
+    & \Or & @{command "unfolding"}~@{text "facts"} \\
     @{text stmt} & = & @{command "{"}~@{text "stmt\<^sup>*"}~@{command "}"} \\
     & \Or & @{command "next"} \\
-    & \Or & @{command "note"}~@{text "name = name\<^sup>+"} \\
+    & \Or & @{command "note"}~@{text "name = facts"} \\
     & \Or & @{command "let"}~@{text "term = term"} \\
     & \Or & @{command "fix"}~@{text "var\<^sup>+"} \\
-    & \Or & @{command "assume"}~@{text "name: prop\<^sup>+"} \\
+    & \Or & @{command "assume"}~@{text "name: props"} \\
     & \Or & @{command "then"}@{text "\<^sup>?"}~@{text goal} \\
-    @{text goal} & = & @{command "have"}~@{text "name: prop\<^sup>+ proof"} \\
-    & \Or & @{command "show"}~@{text "name: prop\<^sup>+ proof"} \\
+    @{text goal} & = & @{command "have"}~@{text "name: props proof"} \\
+    & \Or & @{command "show"}~@{text "name: props proof"} \\
   \end{matharray}
 *}
 
diff -r 35809287ab23 -r de781c5c48c1 doc-src/IsarRef/Thy/document/Quick_Reference.tex
--- a/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Sat May 03 13:26:08 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Quick_Reference.tex	Sat May 03 13:36:11 2008 +0200
@@ -49,21 +49,21 @@
   \end{tabular}
 
   \begin{matharray}{rcl}
-    \isa{theory{\isasymdash}stmt} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{name{\isacharcolon}\ prop\ proof} \Or \mbox{\isa{\isacommand{definition}}}~\dots \Or \dots \\[1ex]
+    \isa{theory{\isasymdash}stmt} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{name{\isacharcolon}\ props\ proof} \Or \mbox{\isa{\isacommand{definition}}}~\dots \Or \dots \\[1ex]
     \isa{proof} & = & \isa{prfx\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{proof}}}~\isa{method\ stmt\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{qed}}}~\isa{method} \\
     & \Or & \isa{prfx\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{done}}} \\[1ex]
     \isa{prfx} & = & \mbox{\isa{\isacommand{apply}}}~\isa{method} \\
-    & \Or & \mbox{\isa{\isacommand{using}}}~\isa{name\isactrlsup {\isacharplus}} \\
-    & \Or & \mbox{\isa{\isacommand{unfolding}}}~\isa{name\isactrlsup {\isacharplus}} \\
+    & \Or & \mbox{\isa{\isacommand{using}}}~\isa{facts} \\
+    & \Or & \mbox{\isa{\isacommand{unfolding}}}~\isa{facts} \\
     \isa{stmt} & = & \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{stmt\isactrlsup {\isacharasterisk}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} \\
     & \Or & \mbox{\isa{\isacommand{next}}} \\
-    & \Or & \mbox{\isa{\isacommand{note}}}~\isa{name\ {\isacharequal}\ name\isactrlsup {\isacharplus}} \\
+    & \Or & \mbox{\isa{\isacommand{note}}}~\isa{name\ {\isacharequal}\ facts} \\
     & \Or & \mbox{\isa{\isacommand{let}}}~\isa{term\ {\isacharequal}\ term} \\
     & \Or & \mbox{\isa{\isacommand{fix}}}~\isa{var\isactrlsup {\isacharplus}} \\
-    & \Or & \mbox{\isa{\isacommand{assume}}}~\isa{name{\isacharcolon}\ prop\isactrlsup {\isacharplus}} \\
+    & \Or & \mbox{\isa{\isacommand{assume}}}~\isa{name{\isacharcolon}\ props} \\
     & \Or & \mbox{\isa{\isacommand{then}}}\isa{\isactrlsup {\isacharquery}}~\isa{goal} \\
-    \isa{goal} & = & \mbox{\isa{\isacommand{have}}}~\isa{name{\isacharcolon}\ prop\isactrlsup {\isacharplus}\ proof} \\
-    & \Or & \mbox{\isa{\isacommand{show}}}~\isa{name{\isacharcolon}\ prop\isactrlsup {\isacharplus}\ proof} \\
+    \isa{goal} & = & \mbox{\isa{\isacommand{have}}}~\isa{name{\isacharcolon}\ props\ proof} \\
+    & \Or & \mbox{\isa{\isacommand{show}}}~\isa{name{\isacharcolon}\ props\ proof} \\
   \end{matharray}%
 \end{isamarkuptext}%
 \isamarkuptrue%