author nipkow Wed Apr 06 18:13:30 2005 +0200 (2005-04-06 ago) changeset 15659 043c460af14d parent 15658 2edb384bf61f child 15660 255055554c67
updated it
```     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:
```