src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 56073 29e308b56d23
parent 55414 eab03e9cee8a
child 56679 5545bfdfefcc
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Mar 12 22:57:50 2014 +0100
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Mar 13 07:07:07 2014 +0100
     1.3 @@ -204,7 +204,6 @@
     1.4      apply auto
     1.5      apply (case_tac xc)
     1.6      apply auto
     1.7 -    apply fastforce
     1.8      done
     1.9  qed
    1.10