src/HOL/HOL.thy
changeset 14248 399a3290936c
parent 14223 0ee05eef881b
child 14295 7f115e5c5de4
     1.1 --- a/src/HOL/HOL.thy	Wed Oct 29 01:17:06 2003 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Oct 29 11:50:26 2003 +0100
     1.3 @@ -540,7 +540,6 @@
     1.4    apply (rule allI)
     1.5    apply (rule ex1I)
     1.6    apply (erule spec)
     1.7 -  apply (rule ccontr)
     1.8    apply (erule_tac x = "%z. if z = x then y else f z" in allE)
     1.9    apply (erule impE)
    1.10    apply (rule allI)