src/HOL/WF.ML
changeset 5143 b94cd208f073
parent 5132 24f992a25adc
child 5148 74919e8f221c
     1.1 --- a/src/HOL/WF.ML	Tue Jul 14 13:33:12 1998 +0200
     1.2 +++ b/src/HOL/WF.ML	Wed Jul 15 10:15:13 1998 +0200
     1.3 @@ -93,7 +93,7 @@
     1.4   * Wellfoundedness of subsets
     1.5   *---------------------------------------------------------------------------*)
     1.6  
     1.7 -Goal "!!r. [| wf(r);  p<=r |] ==> wf(p)";
     1.8 +Goal "[| wf(r);  p<=r |] ==> wf(p)";
     1.9  by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
    1.10  by (Fast_tac 1);
    1.11  qed "wf_subset";
    1.12 @@ -164,7 +164,7 @@
    1.13  by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1);
    1.14  qed "cuts_eq";
    1.15  
    1.16 -Goalw [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
    1.17 +Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)";
    1.18  by (asm_simp_tac HOL_ss 1);
    1.19  qed "cut_apply";
    1.20