author wenzelm Tue, 04 Jul 2006 15:30:30 +0200 changeset 19990 837f1b10722c parent 19989 5e829405e1a8 child 19991 0c9650664d47
--- a/doc-src/IsarRef/refcard.tex	Tue Jul 04 15:30:29 2006 +0200
+++ b/doc-src/IsarRef/refcard.tex	Tue Jul 04 15:30:30 2006 +0200
@@ -10,30 +10,30 @@
$\ASSUME{a}{\vec\phi}$ & augment context by $\vec\phi \Imp \Box$ \\
$\THEN$ & indicate forward chaining of facts \\
$\HAVE{a}{\phi}$ & prove local result \\
-  $\SHOW{a}{\phi}$ & prove local result, establishing some goal \\
+  $\SHOW{a}{\phi}$ & prove local result, refining some goal \\
$\USING{\vec a}$ & indicate use of additional facts \\
-  $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
+  $\UNFOLDING{\vec a}$ & unfold definitional equations \\
+  $\PROOF{m@1}~\dots~\QED{m@2}$ & indicate proof structure and refinements \\
$\BG~\dots~\EN$ & declare explicit blocks \\
-  $\NEXT$ & switch implicit blocks \\
+  $\NEXT$ & switch blocks \\
$\NOTE{a}{\vec b}$ & reconsider facts \\
$\LET{p = t}$ & \Text{abbreviate terms by higher-order matching} \\
\end{tabular}

\begin{matharray}{rcl}
-  theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \\
-  & \Or & \LEMMA{name}{prop}~proof \\
-  & \Or & \TYPES~\dots \Or \CONSTS~\dots \Or \DEFS~\dots \Or \dots \\[1ex]
-  proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\[1ex]
+  theory{\dsh}stmt & = & \THEOREM{name}{prop} ~proof \Or \isarkeyword{definition}~\dots \Or \dots \\[1ex]
+  proof & = & prfx^*~\PROOF{method}~stmt^*~\QED{method} \\
+  & \Or & prfx^*~\DONE \\[1ex]
prfx & = & \APPLY{method} \\
& \Or & \USING{name^+} \\
+  & \Or & \UNFOLDING{name^+} \\
stmt & = & \BG~stmt^*~\EN \\
& \Or & \NEXT \\
& \Or & \NOTE{name}{name^+} \\
-  & \Or & \LET{term = term} \\[0.5ex]
+  & \Or & \LET{term = term} \\
& \Or & \FIX{var^+} \\
& \Or & \ASSUME{name}{prop^+}\\
-  & \Or & \THEN~goal{\dsh}stmt \\
-  & \Or & goal \\
+  & \Or & \THEN^?~goal \\
goal & = & \HAVE{name}{prop}~proof \\
& \Or & \SHOW{name}{prop}~proof \\
\end{matharray}