More robust proof (?)
authorpaulson
Fri Feb 21 15:38:44 1997 +0100 (1997-02-21)
changeset 26731b266c161134
parent 2672 85d7e800d754
child 2674 4385d521a691
More robust proof (?)
src/ZF/upair.ML
     1.1 --- a/src/ZF/upair.ML	Fri Feb 21 15:31:47 1997 +0100
     1.2 +++ b/src/ZF/upair.ML	Fri Feb 21 15:38:44 1997 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4  (*Classical introduction rule*)
     1.5  qed_goal "consCI" thy "(a~:B ==> a=b) ==> a: cons(b,B)"
     1.6   (fn prems=>
     1.7 -  [ Simp_tac 1, fast_tac (!claset addIs prems) 1 ]);
     1.8 +  [ Simp_tac 1, fast_tac (!claset addSIs prems) 1 ]);
     1.9  
    1.10  AddSIs [consCI];
    1.11  AddSEs [consE];