| changeset 4098 | 71e05eb27fb6 |
| parent 3664 | 2dced1ac2d8e |
| child 4423 | a129b817b58a |
--- a/src/HOLCF/IMP/HoareEx.ML Mon Nov 03 12:36:48 1997 +0100 +++ b/src/HOLCF/IMP/HoareEx.ML Mon Nov 03 14:06:27 1997 +0100 @@ -14,6 +14,6 @@ (* simplifier with enhanced adm-tactic: *) by (Simp_tac 1); by (Simp_tac 1); -by (simp_tac (!simpset setloop (split_tac[expand_if])) 1); +by (simp_tac (simpset() setloop (split_tac[expand_if])) 1); by(Blast_tac 1); qed "WHILE_rule_sound";