# HG changeset patch
# User huffman
# Date 1269297727 25200
# Node ID ea0bf2a01eb02848d4ae84b38a75cc23ab2baba7
# Parent  e0382e4b4da79a09a2ea41a5009148f521bd0393
avoid dependence on adm_tac solver

diff -r e0382e4b4da7 -r ea0bf2a01eb0 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Mar 22 15:23:16 2010 -0700
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Mar 22 15:42:07 2010 -0700
@@ -814,9 +814,8 @@
 
 lemma nForall_HDFilter:
  "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"
-(* Pay attention: is only admissible with chain-finite package to be added to
-        adm test *)
-apply (rule_tac x="y" in Seq_induct)
+unfolding not_Undef_is_Def [symmetric]
+apply (induct y rule: Seq_induct)
 apply (simp add: Forall_def sforall_def)
 apply simp_all
 done