summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | prensani |

Fri, 21 Jul 2000 16:35:12 +0200 | |

changeset 9397 | 358e67410253 |

parent 9396 | a1b31d61f8e1 |

child 9398 | 0ee9b2819155 |

Updating of some comments

src/HOL/Hoare/Hoare.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Hoare/Hoare.thy | file | annotate | diff | comparison | revisions |

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