src/FOLP/IFOLP.thy
changeset 56199 8e8d28ed7529
parent 55380 4de48353034e
child 58889 5b7a9633cfa8
     1.1 --- a/src/FOLP/IFOLP.thy	Tue Mar 18 10:00:23 2014 +0100
     1.2 +++ b/src/FOLP/IFOLP.thy	Tue Mar 18 11:07:47 2014 +0100
     1.3 @@ -411,7 +411,7 @@
     1.4    done
     1.5  
     1.6  (*NOT PROVED
     1.7 -bind_thm ("ex1_cong", prove_goal (the_context ())
     1.8 +ML_Thms.bind_thm ("ex1_cong", prove_goal (the_context ())
     1.9      "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))"
    1.10   (fn prems =>
    1.11    [ (REPEAT   (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1