Loading theory "Noninterference_Generic_Unwinding.GenericUnwinding"
Proofs for inductive predicate(s) "rel_induct_auxp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
*** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
***  1. unaffected_domains I D {D y} (ys @ [y']) \<noteq> {}
*** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
*** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
***  1. unaffected_domains I D {D y} (zs @ [z]) \<noteq> {}
*** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
### theory "Noninterference_Generic_Unwinding.GenericUnwinding"
### 1.885s elapsed time, 4.344s cpu time, 0.132s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline -o pdf -n outline -t /proof,/ML
*** Failed to build document in "/media/data/jenkins/workspace/isabelle-all/browser_info/AFP/Noninterference_Generic_Unwinding/outline"
*** Failed to apply initial proof method (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
***  1. unaffected_domains I D {D y} (zs @ [z]) \<noteq> {}
*** At command "proof" (line 787 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")
*** Failed to apply initial proof method (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy"):
*** goal (1 subgoal):
***  1. unaffected_domains I D {D y} (ys @ [y']) \<noteq> {}
*** At command "proof" (line 689 of "$AFP/Noninterference_Generic_Unwinding/GenericUnwinding.thy")