changeset 9190 | b86ff604729f |
parent 8948 | b797cfa3548d |
child 9337 | 58bd51302b21 |
--- a/src/HOL/UNITY/Extend.ML Thu Jun 29 12:17:18 2000 +0200 +++ b/src/HOL/UNITY/Extend.ML Thu Jun 29 12:19:27 2000 +0200 @@ -45,7 +45,7 @@ Goalw [Restrict_def] "[| A <= B; Restrict B r = Restrict B s |] \ \ ==> Restrict A r = Restrict A s"; -by (blast_tac (claset() addSEs [equalityE]) 1); +by (Blast_tac 1); qed "Restrict_eq_mono"; Goalw [Restrict_def, image_def]