updated it
authornipkow
Wed Apr 06 18:13:30 2005 +0200 (2005-04-06 ago)
changeset 15659043c460af14d
parent 15658 2edb384bf61f
child 15660 255055554c67
updated it
src/HOL/Hoare/README.html
     1.1 --- a/src/HOL/Hoare/README.html	Wed Apr 06 12:01:37 2005 +0200
     1.2 +++ b/src/HOL/Hoare/README.html	Wed Apr 06 18:13:30 2005 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  
     1.5  After loading theory Hoare, you can state goals of the form
     1.6  <PRE>
     1.7 -|- VARS x y ... {P} prog {Q}
     1.8 +VARS x y ... {P} prog {Q}
     1.9  </PRE>
    1.10  where <kbd>prog</kbd> is a program in the above language, <kbd>P</kbd> is the
    1.11  precondition, <kbd>Q</kbd> the postcondition, and <kbd>x y ...</kbd> is the
    1.12 @@ -37,7 +37,7 @@
    1.13  be nonempty and it must include all variables that occur on the left-hand
    1.14  side of an assignment in <kbd>prog</kbd>. Example:
    1.15  <PRE>
    1.16 -|- VARS x. {x = a} x := x+1 {x = a+1}
    1.17 +VARS x {x = a} x := x+1 {x = a+1}
    1.18  </PRE>
    1.19  The (normal) variable <kbd>a</kbd> is merely used to record the initial
    1.20  value of <kbd>x</kbd> and is not a program variable. Pre/post conditions
    1.21 @@ -46,19 +46,18 @@
    1.22  <P>
    1.23  
    1.24  The implementation hides reasoning in Hoare logic completely and provides a
    1.25 -tactic <kbd>hoare_tac</kbd> for transforming a goal in Hoare logic into an
    1.26 +method <kbd>vcg</kbd> for transforming a goal in Hoare logic into an
    1.27  equivalent list of verification conditions in HOL:
    1.28  <PRE>
    1.29 -by(hoare_tac tac i);
    1.30 +apply vcg
    1.31  </PRE>
    1.32 -applies the tactic to subgoal <kbd>i</kbd> and applies the parameter
    1.33 -<kbd>tac</kbd> (of type <kbd>int -&gt; tactic</kbd>) to all generated
    1.34 -verification conditions. A typical call is
    1.35 +If you want to simplify the resulting verification conditions at the same
    1.36 +time:
    1.37  <PRE>
    1.38 -by(hoare_tac Asm_full_simp_tac 1);
    1.39 +apply vcg_simp
    1.40  </PRE>
    1.41  which, given the example goal above, solves it completely. For further
    1.42 -examples see <a href="Examples.ML">Examples.ML</a>.
    1.43 +examples see <a href="Examples.html">Examples</a>.
    1.44  <P>
    1.45  
    1.46  IMPORTANT: