--- 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
--- 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"