'using' primitive;
authorwenzelm
Mon Mar 04 22:32:15 2002 +0100 (2002-03-04)
changeset 13017c28df0f7ebdb
parent 13016 c039b8ede204
child 13018 5164177cf0a6
'using' primitive;
doc-src/IsarRef/refcard.tex
     1.1 --- a/doc-src/IsarRef/refcard.tex	Mon Mar 04 22:31:21 2002 +0100
     1.2 +++ b/doc-src/IsarRef/refcard.tex	Mon Mar 04 22:32:15 2002 +0100
     1.3 @@ -8,9 +8,10 @@
     1.4  \begin{tabular}{ll}
     1.5    $\FIX{\vec x}$ & augment context by $\All {\vec x} \Box$ \\
     1.6    $\ASSUME{a}{\vec\phi}$ & augment context by $\vec\phi \Imp \Box$ \\
     1.7 -  $\THEN$ & indicate forward chaining \\
     1.8 +  $\THEN$ & indicate forward chaining of facts \\
     1.9    $\HAVE{a}{\phi}$ & prove local result \\
    1.10    $\SHOW{a}{\phi}$ & prove local result, establishing some goal \\
    1.11 +  $\USING{\vec a}$ & indicate use of additional facts \\
    1.12    $\PROOF{m@1}~\dots~\QED{m@2}$ & apply proof methods \\
    1.13    $\BG~\dots~\EN$ & declare explicit blocks \\
    1.14    $\NEXT$ & switch implicit blocks \\