doc-src/IsarImplementation/Thy/unused.thy
changeset 20474 af069653f1d7
parent 20470 c839b38a1f32
child 20477 e623b0e30541
     1.1 --- a/doc-src/IsarImplementation/Thy/unused.thy	Mon Sep 04 18:41:33 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/unused.thy	Mon Sep 04 19:49:39 2006 +0200
     1.3 @@ -1,6 +1,24 @@
     1.4  
     1.5  text {*
     1.6  
     1.7 +
     1.8 +  \medskip The general concept supports block-structured reasoning
     1.9 +  nicely, with arbitrary mechanisms for introducing local assumptions.
    1.10 +  The common reasoning pattern is as follows:
    1.11 +
    1.12 +  \medskip
    1.13 +  \begin{tabular}{l}
    1.14 +  @{text "add_assms e\<^isub>1 A\<^isub>1"} \\
    1.15 +  @{text "\<dots>"} \\
    1.16 +  @{text "add_assms e\<^isub>n A\<^isub>n"} \\
    1.17 +  @{text "export"} \\
    1.18 +  \end{tabular}
    1.19 +  \medskip
    1.20 +
    1.21 +  \noindent The final @{text "export"} will turn any fact @{text
    1.22 +  "A\<^isub>1, \<dots>, A\<^isub>n \<turnstile> B"} into some @{text "\<turnstile> B'"}, by
    1.23 +  applying the export rules @{text "e\<^isub>1, \<dots>, e\<^isub>n"}
    1.24 +  inside-out.
    1.25    
    1.26  
    1.27    A \emph{fixed variable} acts like a local constant in the current