# HG changeset patch
# User prensani
# Date 964190112 -7200
# Node ID 358e6741025324edf408152cf64900d70d67fc42
# Parent  a1b31d61f8e124e04c742afc9d4ac2262e9f87cd
Updating of some comments

diff -r a1b31d61f8e1 -r 358e67410253 src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Fri Jul 21 12:30:08 2000 +0200
+++ b/src/HOL/Hoare/Hoare.ML	Fri Jul 21 16:35:12 2000 +0200
@@ -61,8 +61,7 @@
 (** The function Mset makes the theorem                                     **)
 (** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}",        **)
 (** where (x1,...,xn) are the variables of the particular program we are    **)
-(** working on at the moment of the call. For instance, (found,x,y) are     **)
-(** the variables of the Zero Search program.                               **)
+(** working on at the moment of the call                                    **)
 (*****************************************************************************)
 
 local open HOLogic in
diff -r a1b31d61f8e1 -r 358e67410253 src/HOL/Hoare/Hoare.thy
--- a/src/HOL/Hoare/Hoare.thy	Fri Jul 21 12:30:08 2000 +0200
+++ b/src/HOL/Hoare/Hoare.thy	Fri Jul 21 16:35:12 2000 +0200
@@ -83,7 +83,7 @@
 
 
 (* bexp_tr & assn_tr *)
-(*all meta-variables for bexp except for TRUE and FALSE are translated as if they
+(*all meta-variables for bexp except for TRUE are translated as if they
   were boolean expressions*)
   
 fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE"