Loading theory "HOL-Library.Lattice_Syntax" (required by "Buchi_Complementation.Complementation_Implement")
Loading theory "Buchi_Complementation.Alternate" (required by "Buchi_Complementation.Complementation" via "Buchi_Complementation.Ranking")
### theory "HOL-Library.Lattice_Syntax"
### 0.014s elapsed time, 0.044s cpu time, 0.000s GC time
Loading theory "HOL-Library.Permutation" (required by "Buchi_Complementation.Complementation_Final")
consts
  alternate ::
    "('a \<Rightarrow> 'a)
     \<Rightarrow> ('a \<Rightarrow> 'a)
                   \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
Proofs for inductive predicate(s) "perm"
### theory "Buchi_Complementation.Alternate"
### 0.094s elapsed time, 0.272s cpu time, 0.000s GC time
Loading theory "Buchi_Complementation.Graph" (required by "Buchi_Complementation.Complementation" via "Buchi_Complementation.Ranking")
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### Ignoring duplicate safe introduction (intro!)
### ?xs <~~> ?ys \<Longrightarrow> ?z # ?xs <~~> ?z # ?ys
### Ignoring duplicate safe introduction (intro!)
### ?xs <~~> ?ys \<Longrightarrow> ?z # ?xs <~~> ?z # ?ys
### theory "HOL-Library.Permutation"
### 0.215s elapsed time, 0.492s cpu time, 0.000s GC time
### theory "Buchi_Complementation.Graph"
### 0.430s elapsed time, 0.916s cpu time, 0.000s GC time
Loading theory "Buchi_Complementation.Ranking" (required by "Buchi_Complementation.Complementation")
### theory "Buchi_Complementation.Ranking"
### 0.939s elapsed time, 1.872s cpu time, 0.000s GC time
Loading theory "Buchi_Complementation.Complementation"
### theory "Buchi_Complementation.Complementation"
### 0.953s elapsed time, 1.824s cpu time, 0.352s GC time
Loading theory "Buchi_Complementation.Complementation_Implement"
### theory "Buchi_Complementation.Complementation_Implement"
### 3.149s elapsed time, 6.224s cpu time, 0.536s GC time
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Buchi_Complementation/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/Buchi_Complementation/outline -o pdf -n outline -t /proof,/ML
*** Failed to load theory "Buchi_Complementation.Complementation_Final" (unresolved "Buchi_Complementation.Complementation_Implement")
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:
***   FOREACH (map_to_set f) (\<lambda>(p, k, c) m. do {
***                                ASSERT (p \<notin> dom m);
***                                RETURN (m(p \<mapsto> (k, True)))
***                              }) ::
***   ('state \<Rightarrow> (nat \<times> bool) option)
***   \<Rightarrow> ('state \<Rightarrow> (nat \<times> bool) option) nres
*** Operand:   {} :: ??'a set
*** 
*** Coercion Inference:
*** 
*** Local coercion insertion on the operand failed:
*** No coercion known for type constructors: "set" and "fun"
*** At command "definition" (line 405 of "~~/afp/thys/Buchi_Complementation/Complementation_Implement.thy")