changeset 9190 | b86ff604729f |
parent 9083 | b36787a56a1f |
child 9337 | 58bd51302b21 |
--- a/src/HOL/UNITY/Project.ML Thu Jun 29 12:17:18 2000 +0200 +++ b/src/HOL/UNITY/Project.ML Thu Jun 29 12:19:27 2000 +0200 @@ -435,7 +435,7 @@ extend_set_Un_distrib]) 2); by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2); by (full_simp_tac (simpset() addsimps [extend_set_def]) 1); -by (blast_tac (claset() addSEs [equalityE]) 1); +by (Blast_tac 1); (*The transient part*) by Auto_tac; by (force_tac (claset() addSDs [equalityD1]