src/HOL/simpdata.ML
changeset 9876 a069795f1060
parent 9875 c50349d252b7
child 9894 c8ff37b637a7
     1.1 --- a/src/HOL/simpdata.ML	Wed Sep 06 13:32:25 2000 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Wed Sep 06 16:54:12 2000 +0200
     1.3 @@ -496,7 +496,7 @@
     1.4     ref_tac: int -> tactic
     1.5     the actual refutation tactic. Should be able to deal with goals
     1.6     [| A1; ...; An |] ==> False
     1.7 -   where the Ai are atomic, i.e. no top-level &, | or ?
     1.8 +   where the Ai are atomic, i.e. no top-level &, | or EX
     1.9  *)
    1.10  
    1.11  fun refute_tac test prep_tac ref_tac =