src/HOL/Set.thy
changeset 26480 544cef16045b
parent 26339 7825c83c9eff
child 26513 6f306c8c2c54
     1.1 --- a/src/HOL/Set.thy	Sat Mar 29 19:13:58 2008 +0100
     1.2 +++ b/src/HOL/Set.thy	Sat Mar 29 19:14:00 2008 +0100
     1.3 @@ -473,7 +473,7 @@
     1.4  lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)"
     1.5    by blast
     1.6  
     1.7 -ML_setup {*
     1.8 +ML {*
     1.9    local
    1.10      val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
    1.11      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;