src/HOL/ex/MT.ML
changeset 5143 b94cd208f073
parent 5069 3ea049f7979d
child 5148 74919e8f221c
     1.1 --- a/src/HOL/ex/MT.ML	Tue Jul 14 13:33:12 1998 +0200
     1.2 +++ b/src/HOL/ex/MT.ML	Wed Jul 15 10:15:13 1998 +0200
     1.3 @@ -574,7 +574,7 @@
     1.4  
     1.5  (* Introduction rules for hasty *)
     1.6  
     1.7 -Goalw [hasty_def] "!!c. c isof t ==> v_const(c) hasty t";
     1.8 +Goalw [hasty_def] "c isof t ==> v_const(c) hasty t";
     1.9  by (etac hasty_rel_const_coind 1);
    1.10  qed "hasty_const";
    1.11  
    1.12 @@ -592,7 +592,7 @@
    1.13  by (ALLGOALS (blast_tac (v_ext_cs HOL_cs)));
    1.14  qed "hasty_elim_const_lem";
    1.15  
    1.16 -Goal "!!c. v_const(c) hasty t ==> c isof t";
    1.17 +Goal "v_const(c) hasty t ==> c isof t";
    1.18  by (dtac hasty_elim_const_lem 1);
    1.19  by (Blast_tac 1);
    1.20  qed "hasty_elim_const";