equal
deleted
inserted
replaced
59 |
59 |
60 (*****************************************************************************) |
60 (*****************************************************************************) |
61 (** The function Mset makes the theorem **) |
61 (** The function Mset makes the theorem **) |
62 (** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}", **) |
62 (** "?Mset <= {(x1,...,xn). ?P (x1,...,xn)} ==> ?Mset <= {s. ?P s}", **) |
63 (** where (x1,...,xn) are the variables of the particular program we are **) |
63 (** where (x1,...,xn) are the variables of the particular program we are **) |
64 (** working on at the moment of the call. For instance, (found,x,y) are **) |
64 (** working on at the moment of the call **) |
65 (** the variables of the Zero Search program. **) |
|
66 (*****************************************************************************) |
65 (*****************************************************************************) |
67 |
66 |
68 local open HOLogic in |
67 local open HOLogic in |
69 |
68 |
70 (** maps (%x1 ... xn. t) to [x1,...,xn] **) |
69 (** maps (%x1 ... xn. t) to [x1,...,xn] **) |