Loading theory "Jinja.Auxiliary" (required by "Jinja.Jinja" via "Jinja.TypeSafe" via "Jinja.Progress" via "Jinja.Equivalence" via "Jinja.BigStep" via "Jinja.Expr" via "Jinja.Exceptions" via "Jinja.Objects" via "Jinja.TypeRel" via "Jinja.Decl" via "Jinja.Type")
Loading theory "Jinja.Semilat" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV" via "Jinja.Typing_Framework_err" via "Jinja.Typing_Framework" via "Jinja.Semilattices" via "Jinja.Err")
### Ignoring duplicate safe elimination (elim!)
### \<lbrakk>?x # ?xs = map ?f ?ys;
###  \<exists>z zs.
###     ?ys = z # zs \<and> ?x = ?f z \<and> ?xs = map ?f zs \<Longrightarrow>
###  PROP ?W\<rbrakk>
### \<Longrightarrow> PROP ?W
### Ignoring duplicate safe elimination (elim!)
### \<lbrakk>?x # ?xs = map ?f ?ys;
###  \<exists>z zs.
###     ?ys = z # zs \<and> ?x = ?f z \<and> ?xs = map ?f zs \<Longrightarrow>
###  PROP ?W\<rbrakk>
### \<Longrightarrow> PROP ?W
### theory "Jinja.Auxiliary"
### 0.194s elapsed time, 0.472s cpu time, 0.000s GC time
Loading theory "Jinja.Type" (required by "Jinja.Jinja" via "Jinja.TypeSafe" via "Jinja.Progress" via "Jinja.Equivalence" via "Jinja.BigStep" via "Jinja.Expr" via "Jinja.Exceptions" via "Jinja.Objects" via "Jinja.TypeRel" via "Jinja.Decl")
locale Semilat
  fixes A :: "'a set"
    and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes "Semilat A r f"
### theory "Jinja.Semilat"
### 0.514s elapsed time, 1.092s cpu time, 0.000s GC time
Loading theory "Jinja.Err" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV" via "Jinja.Typing_Framework_err" via "Jinja.Typing_Framework" via "Jinja.Semilattices")
### theory "Jinja.Type"
### 0.715s elapsed time, 1.436s cpu time, 0.000s GC time
Loading theory "Jinja.Decl" (required by "Jinja.Jinja" via "Jinja.TypeSafe" via "Jinja.Progress" via "Jinja.Equivalence" via "Jinja.BigStep" via "Jinja.Expr" via "Jinja.Exceptions" via "Jinja.Objects" via "Jinja.TypeRel")
### theory "Jinja.Decl"
### 0.083s elapsed time, 0.168s cpu time, 0.000s GC time
Loading theory "Jinja.TypeRel" (required by "Jinja.Jinja" via "Jinja.TypeSafe" via "Jinja.Progress" via "Jinja.Equivalence" via "Jinja.BigStep" via "Jinja.Expr" via "Jinja.Exceptions" via "Jinja.Objects")
### No equation for constructor "Err"
consts
  ok_val :: "'a err \<Rightarrow> 'a"
Proofs for inductive predicate(s) "subcls1p"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  strict ::
    "('a \<Rightarrow> 'b err) \<Rightarrow> 'a err \<Rightarrow> 'b err"
Proofs for inductive predicate(s) "widen"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "Methods"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### theory "Jinja.Err"
### 1.017s elapsed time, 2.040s cpu time, 0.000s GC time
Loading theory "Jinja.Listn" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV" via "Jinja.Typing_Framework_err" via "Jinja.Typing_Framework" via "Jinja.Semilattices")
consts
  coalesce :: "'a err list \<Rightarrow> 'a list err"
Proofs for inductive predicate(s) "Fields"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
### Introduced fixed type variable(s): 'a in "y"
### Introduced fixed type variable(s): 'a in "z"
### theory "Jinja.Listn"
### 0.727s elapsed time, 1.404s cpu time, 0.504s GC time
Loading theory "Jinja.Opt" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV" via "Jinja.Typing_Framework_err" via "Jinja.Typing_Framework" via "Jinja.Semilattices")
### theory "Jinja.Opt"
### 0.135s elapsed time, 0.272s cpu time, 0.000s GC time
Loading theory "Jinja.Product" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV" via "Jinja.Typing_Framework_err" via "Jinja.Typing_Framework" via "Jinja.Semilattices")
### theory "Jinja.Product"
### 0.121s elapsed time, 0.244s cpu time, 0.000s GC time
Loading theory "Jinja.Semilattices" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV" via "Jinja.Typing_Framework_err" via "Jinja.Typing_Framework")
### theory "Jinja.TypeRel"
### 1.812s elapsed time, 3.580s cpu time, 0.504s GC time
Loading theory "Jinja.Value" (required by "Jinja.Jinja" via "Jinja.TypeSafe" via "Jinja.Progress" via "Jinja.Equivalence" via "Jinja.BigStep" via "Jinja.Expr" via "Jinja.Exceptions" via "Jinja.Objects")
### theory "Jinja.Semilattices"
### 0.342s elapsed time, 0.684s cpu time, 0.000s GC time
Loading theory "Jinja.Typing_Framework" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV" via "Jinja.Typing_Framework_err")
### theory "Jinja.Typing_Framework"
### 0.068s elapsed time, 0.136s cpu time, 0.000s GC time
Loading theory "Jinja.SemilatAlg" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV" via "Jinja.Typing_Framework_err")
consts
  pluslussub ::
    "'a list
     \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a)
                   \<Rightarrow> 'a \<Rightarrow> 'a"
### theory "Jinja.SemilatAlg"
### 0.172s elapsed time, 0.344s cpu time, 0.000s GC time
Loading theory "Jinja.Kildall" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV")
consts
  propa ::
    "('s \<Rightarrow> 's \<Rightarrow> 's)
     \<Rightarrow> (nat \<times> 's) list
                   \<Rightarrow> 's list
                                 \<Rightarrow> nat set
         \<Rightarrow> 's list \<times> nat set"
consts
  merges ::
    "('s \<Rightarrow> 's \<Rightarrow> 's)
     \<Rightarrow> (nat \<times> 's) list
                   \<Rightarrow> 's list \<Rightarrow> 's list"
### No equation for constructor "Unit"
### No equation for constructor "Null"
### No equation for constructor "Bool"
### No equation for constructor "Addr"
consts
  the_Intg :: "val \<Rightarrow> int"
### No equation for constructor "Unit"
### No equation for constructor "Null"
### No equation for constructor "Bool"
### No equation for constructor "Intg"
consts
  the_Addr :: "val \<Rightarrow> nat"
consts
  default_val :: "ty \<Rightarrow> val"
### theory "Jinja.Value"
### 0.606s elapsed time, 1.216s cpu time, 0.000s GC time
Loading theory "Jinja.Objects" (required by "Jinja.Jinja" via "Jinja.TypeSafe" via "Jinja.Progress" via "Jinja.Equivalence" via "Jinja.BigStep" via "Jinja.Expr" via "Jinja.Exceptions")
### theory "Jinja.Kildall"
### 0.382s elapsed time, 0.764s cpu time, 0.000s GC time
Loading theory "Jinja.LBVSpec" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV" via "Jinja.LBVCorrect")
consts
  typeof_h ::
    "(nat
      \<Rightarrow> (char list \<times>
                     (char list \<times> char list
                      \<Rightarrow> val option)) option)
     \<Rightarrow> val \<Rightarrow> ty option"
consts
  merge ::
    "'s list
     \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> 's)
                   \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool)
                                 \<Rightarrow> 's
         \<Rightarrow> nat
                       \<Rightarrow> (nat \<times> 's) list
                                     \<Rightarrow> 's \<Rightarrow> 's"
### theory "Jinja.Objects"
### 0.173s elapsed time, 0.348s cpu time, 0.000s GC time
Loading theory "Jinja.Typing_Framework_err" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV")
consts
  wtl_inst_list ::
    "'a list
     \<Rightarrow> 's list
                   \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> 's)
                                 \<Rightarrow> ('s
          \<Rightarrow> 's \<Rightarrow> bool)
         \<Rightarrow> 's \<Rightarrow> 's
  \<Rightarrow> (nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list)
                \<Rightarrow> nat \<Rightarrow> 's \<Rightarrow> 's"
locale lbv
  fixes A :: "'a set"
    and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and T :: "'a"  ("\<top>")
    and B :: "'a"  ("\<bottom>")
    and step :: "nat \<Rightarrow> 'a \<Rightarrow> (nat \<times> 'a) list"
    and
    merge ::
      "'a list
       \<Rightarrow> nat
                     \<Rightarrow> (nat \<times> 'a) list
                                   \<Rightarrow> 'a \<Rightarrow> 'a"
    and wti :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    and wtc :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    and
    wtl ::
      "'b list
       \<Rightarrow> 'a list
                     \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes "lbv A r f \<top> \<bottom>"
  defines "\<And>cert. merge cert \<equiv> merge cert f r \<top>"
    and "\<And>cert. wti cert \<equiv> wtl_inst cert f r \<top> step"
    and
    "\<And>cert. wtc cert \<equiv> wtl_cert cert f r \<top> \<bottom> step"
    and
    "\<And>ins cert.
        wtl ins cert \<equiv>
        wtl_inst_list ins cert f r \<top> \<bottom> step"
### theory "Jinja.Typing_Framework_err"
### 0.220s elapsed time, 0.436s cpu time, 0.000s GC time
Loading theory "List-Index.List_Index" (required by "Jinja.Jinja" via "Jinja.TypeComp" via "Jinja.Compiler" via "Jinja.Correctness1" via "Jinja.Compiler1" via "Jinja.Hidden")
consts
  find_index ::
    "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
consts
  map_index' ::
    "nat
     \<Rightarrow> (nat \<Rightarrow> 'a \<Rightarrow> 'b)
                   \<Rightarrow> 'a list \<Rightarrow> 'b list"
### theory "Jinja.LBVSpec"
### 0.710s elapsed time, 1.416s cpu time, 0.000s GC time
Loading theory "Jinja.LBVComplete" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV")
consts
  insert_nth ::
    "nat \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
locale lbvc
  fixes A :: "'a set"
    and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and T :: "'a"  ("\<top>")
    and B :: "'a"  ("\<bottom>")
    and step :: "nat \<Rightarrow> 'a \<Rightarrow> (nat \<times> 'a) list"
    and
    merge ::
      "'a list
       \<Rightarrow> nat
                     \<Rightarrow> (nat \<times> 'a) list
                                   \<Rightarrow> 'a \<Rightarrow> 'a"
    and wti :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    and wtc :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    and
    wtl ::
      "'b list
       \<Rightarrow> 'a list
                     \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    and \<tau>s :: "'a list"
    and c :: "'a list"
  assumes "lbvc A r f \<top> \<bottom> step \<tau>s"
  defines "\<And>cert. merge cert \<equiv> merge cert f r \<top>"
    and "\<And>cert. wti cert \<equiv> wtl_inst cert f r \<top> step"
    and
    "\<And>cert. wtc cert \<equiv> wtl_cert cert f r \<top> \<bottom> step"
    and
    "\<And>ins cert.
        wtl ins cert \<equiv>
        wtl_inst_list ins cert f r \<top> \<bottom> step"
    and "c \<equiv> make_cert step \<tau>s \<bottom>"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
### theory "List-Index.List_Index"
### 0.719s elapsed time, 1.428s cpu time, 0.000s GC time
Loading theory "Jinja.LBVCorrect" (required by "Jinja.Jinja" via "Jinja.BVExec" via "Jinja.Abstract_BV")
locale lbvs
  fixes A :: "'a set"
    and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    and T :: "'a"  ("\<top>")
    and B :: "'a"  ("\<bottom>")
    and step :: "nat \<Rightarrow> 'a \<Rightarrow> (nat \<times> 'a) list"
    and
    merge ::
      "'a list
       \<Rightarrow> nat
                     \<Rightarrow> (nat \<times> 'a) list
                                   \<Rightarrow> 'a \<Rightarrow> 'a"
    and wti :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    and wtc :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    and
    wtl ::
      "'b list
       \<Rightarrow> 'a list
                     \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    and s\<^sub>0 :: "'a"
    and c :: "'a list"
    and ins :: "'b list"
    and \<tau>s :: "'a list"
  assumes "lbvs A r f \<top> \<bottom> step c ins"
  defines "\<And>cert. merge cert \<equiv> merge cert f r \<top>"
    and "\<And>cert. wti cert \<equiv> wtl_inst cert f r \<top> step"
    and
    "\<And>cert. wtc cert \<equiv> wtl_cert cert f r \<top> \<bottom> step"
    and
    "\<And>ins cert.
        wtl ins cert \<equiv>
        wtl_inst_list ins cert f r \<top> \<bottom> step"
    and
    "\<tau>s \<equiv>
     map (\<lambda>pc.
             if c ! pc = \<bottom> then wtl (take pc ins) c 0 s\<^sub>0
             else c ! pc)
      [0..<length ins]"
### theory "Jinja.LBVComplete"
### 0.446s elapsed time, 0.884s cpu time, 0.000s GC time
Loading theory "Jinja.Hidden" (required by "Jinja.Jinja" via "Jinja.TypeComp" via "Jinja.Compiler" via "Jinja.Correctness1" via "Jinja.Compiler1")
### theory "Jinja.Hidden"
### 0.076s elapsed time, 0.148s cpu time, 0.000s GC time
### Ignoring duplicate rewrite rule:
### (?f1(?x1 := ?y1)) ?z1 \<equiv> if ?z1 = ?x1 then ?y1 else ?f1 ?z1
### theory "Jinja.LBVCorrect"
### 0.667s elapsed time, 1.268s cpu time, 0.668s GC time
Loading theory "Jinja.Abstract_BV" (required by "Jinja.Jinja" via "Jinja.BVExec")
### theory "Jinja.Abstract_BV"
### 0.406s elapsed time, 0.816s cpu time, 0.000s GC time
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  ?Q C C Mm ::
***   (char list
***    \<Rightarrow> ((ty list \<times> ty \<times> 'a) \<times>
***                   char list) option)
***   \<Rightarrow> bool
*** Operand:   {} :: ??'a set
*** 
*** At command "hence" (line 244 of "~~/afp/thys/Jinja/Common/TypeRel.thy")
### Ignoring duplicate rewrite rule:
### (?f1(?x1 := ?y1)) ?z1 \<equiv> if ?z1 = ?x1 then ?y1 else ?f1 ?z1
### Induction variable occurs also among premises: "n" (line 409 of "~~/afp/thys/Jinja/DFA/Listn.thy")
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Rule already declared as introduction (intro)
### (\<And>x. ?f x = ?g x) \<Longrightarrow> ?f = ?g
### Ignoring duplicate rewrite rule:
### Sup ?A1 \<equiv> True \<in> ?A1
### Ignoring duplicate rewrite rule:
### Sup ?A1 \<equiv> True \<in> ?A1
### Ambiguous input (line 94 of "~~/afp/thys/Jinja/DFA/SemilatAlg.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.member"
###     ("\<^const>SemilatAlg.pluslussub"
###       ("\<^const>List.list.Cons" ("_position" x) ("_position" xs))
###       ("_position" f) ("_position" y))
###     ("_position" A)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.member"
###     ("\<^const>List.list.Cons" ("_position" x)
###       ("\<^const>SemilatAlg.pluslussub" ("_position" xs) ("_position" f)
###         ("_position" y)))
###     ("_position" A)))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ignoring duplicate safe introduction (intro!)
### \<lbrakk>?A \<subseteq> ?B; ?A \<noteq> ?B\<rbrakk>
### \<Longrightarrow> ?A \<subset> ?B
### Ignoring duplicate rewrite rule:
### \<lbrakk>order ?r1; Semilat.top ?r1 ?T1\<rbrakk>
### \<Longrightarrow> ?T1 \<sqsubseteq>\<^bsub>?r1\<^esub> ?x1 \<equiv>
###                   ?x1 = ?T1
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jinja/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Jinja/outline -o pdf -n outline -t /proof,/ML
*** Failed to load theory "Jinja.Exceptions" (unresolved "Jinja.Objects")
*** Failed to load theory "Jinja.Conform" (unresolved "Jinja.Exceptions")
*** Failed to load theory "Jinja.Expr" (unresolved "Jinja.Exceptions")
*** Failed to load theory "Jinja.Examples" (unresolved "Jinja.Expr")
*** Failed to load theory "Jinja.State" (unresolved "Jinja.Exceptions")
*** Failed to load theory "Jinja.BigStep" (unresolved "Jinja.Expr", "Jinja.State")
*** Failed to load theory "Jinja.DefAss" (unresolved "Jinja.BigStep")
*** Failed to load theory "Jinja.J1" (unresolved "Jinja.BigStep")
*** Failed to load theory "Jinja.execute_Bigstep" (unresolved "Jinja.BigStep", "Jinja.Examples")
*** Failed to load theory "Jinja.SmallStep" (unresolved "Jinja.Expr", "Jinja.State")
*** Failed to load theory "Jinja.SystemClasses" (unresolved "Jinja.Exceptions")
*** Failed to load theory "Jinja.JVMState" (unresolved "Jinja.Objects")
*** Failed to load theory "Jinja.JVMInstructions" (unresolved "Jinja.JVMState")
*** Failed to load theory "Jinja.JVMExceptions" (unresolved "Jinja.Exceptions", "Jinja.JVMInstructions")
*** Failed to load theory "Jinja.JVMExecInstr" (unresolved "Jinja.Exceptions", "Jinja.JVMInstructions", "Jinja.JVMState")
*** Failed to load theory "Jinja.JVMExec" (unresolved "Jinja.JVMExceptions", "Jinja.JVMExecInstr")
*** Failed to load theory "Jinja.JVMDefensive" (unresolved "Jinja.Conform", "Jinja.JVMExec")
*** Failed to load theory "Jinja.JVMListExample" (unresolved "Jinja.JVMExec", "Jinja.SystemClasses")
*** Failed to load theory "Jinja.WellType" (unresolved "Jinja.Expr", "Jinja.Objects")
*** Failed to load theory "Jinja.Annotate" (unresolved "Jinja.WellType")
*** Failed to load theory "Jinja.WellTypeRT" (unresolved "Jinja.WellType")
*** Failed to load theory "Jinja.execute_WellType" (unresolved "Jinja.Examples", "Jinja.WellType")
*** Failed to load theory "Jinja.WellForm" (unresolved "Jinja.SystemClasses")
*** Failed to load theory "Jinja.PCompiler" (unresolved "Jinja.WellForm")
*** Failed to load theory "Jinja.Compiler2" (unresolved "Jinja.J1", "Jinja.JVMExec", "Jinja.PCompiler")
*** Failed to load theory "Jinja.Correctness2" (unresolved "Jinja.Compiler2")
*** Failed to load theory "Jinja.WWellForm" (unresolved "Jinja.Expr", "Jinja.WellForm")
*** Failed to load theory "Jinja.Equivalence" (unresolved "Jinja.BigStep", "Jinja.SmallStep", "Jinja.WWellForm")
*** Failed to load theory "Jinja.Progress" (unresolved "Jinja.Conform", "Jinja.DefAss", "Jinja.Equivalence", "Jinja.WellTypeRT")
*** Failed to load theory "Jinja.JWellForm" (unresolved "Jinja.DefAss", "Jinja.WWellForm", "Jinja.WellForm", "Jinja.WellType")
*** Failed to load theory "Jinja.J1WellForm" (unresolved "Jinja.J1", "Jinja.JWellForm")
*** Failed to load theory "Jinja.TypeSafe" (unresolved "Jinja.JWellForm", "Jinja.Progress")
*** Failed to load theory "Jinja.SemiType" (unresolved "Jinja.WellForm")
*** Failed to load theory "Jinja.JVM_SemiType" (unresolved "Jinja.SemiType")
*** Failed to load theory "Jinja.Effect" (unresolved "Jinja.JVMExceptions", "Jinja.JVM_SemiType")
*** Failed to load theory "Jinja.BVSpec" (unresolved "Jinja.Effect")
*** Failed to load theory "Jinja.BVConform" (unresolved "Jinja.BVSpec", "Jinja.Conform", "Jinja.JVMExec")
*** Failed to load theory "Jinja.BVSpecTypeSafe" (unresolved "Jinja.BVConform")
*** Failed to load theory "Jinja.BVNoTypeError" (unresolved "Jinja.BVSpecTypeSafe", "Jinja.JVMDefensive")
*** Failed to load theory "Jinja.EffectMono" (unresolved "Jinja.Effect")
*** Failed to load theory "Jinja.TF_JVM" (unresolved "Jinja.BVSpec", "Jinja.EffectMono")
*** Failed to load theory "Jinja.Compiler1" (unresolved "Jinja.J1", "Jinja.PCompiler")
*** Failed to load theory "Jinja.Correctness1" (unresolved "Jinja.Compiler1", "Jinja.J1WellForm")
*** Failed to load theory "Jinja.Compiler" (unresolved "Jinja.Correctness1", "Jinja.Correctness2")
*** Failed to load theory "Jinja.TypeComp" (unresolved "Jinja.BVSpec", "Jinja.Compiler")
*** Failed to load theory "Jinja.BVExec" (unresolved "Jinja.TF_JVM")
*** Failed to load theory "Jinja.BVExample" (unresolved "Jinja.BVExec", "Jinja.BVSpecTypeSafe", "Jinja.JVMListExample")
*** Failed to load theory "Jinja.LBVJVM" (unresolved "Jinja.TF_JVM")
*** Failed to load theory "Jinja.Jinja" (unresolved "Jinja.Annotate", "Jinja.BVExample", "Jinja.BVExec", "Jinja.BVNoTypeError", "Jinja.JVMDefensive", "Jinja.JVMListExample", "Jinja.LBVJVM", "Jinja.TypeComp", "Jinja.TypeSafe", "Jinja.execute_Bigstep", "Jinja.execute_WellType")
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  ?Q C C Mm ::
***   (char list
***    \<Rightarrow> ((ty list \<times> ty \<times> 'a) \<times>
***                   char list) option)
***   \<Rightarrow> bool
*** Operand:   {} :: ??'a set
*** 
*** At command "hence" (line 244 of "~~/afp/thys/Jinja/Common/TypeRel.thy")
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  typeof_h ::
***   (nat
***    \<Rightarrow> (char list \<times>
***                   (char list \<times> char list
***                    \<Rightarrow> val option)) option)
***   \<Rightarrow> val \<Rightarrow> ty option
*** Operand:   {} :: ??'a set
*** 
*** At command "abbreviation" (line 84 of "~~/afp/thys/Jinja/Common/Objects.thy")