changeset 13630 | a013a9dd370f |
parent 9747 | 043098ba5098 |
1.1 --- a/src/HOL/MiniML/MiniML.ML Mon Oct 07 19:01:51 2002 +0200 1.2 +++ b/src/HOL/MiniML/MiniML.ML Tue Oct 08 08:20:17 2002 +0200 1.3 @@ -90,7 +90,6 @@ 1.4 by (rtac ballI 1); 1.5 by (etac UN_E 1); 1.6 by (dtac (dom_S' RS subsetD) 1); 1.7 -by (rotate_tac 1 1); 1.8 by (Asm_full_simp_tac 1); 1.9 by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_scheme_lists] 1.10 addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1);