Loading theory "FeatherweightJava.FJDefs" (required by "FeatherweightJava.Featherweight_Java" via "FeatherweightJava.FJSound" via "FeatherweightJava.FJAux")
Proofs for inductive predicate(s) "isubexprsp"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
Proofs for inductive predicate(s) "vals", "val"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
consts
  substs ::
    "(nat \<Rightarrow> exp option) \<Rightarrow> exp \<Rightarrow> exp"
  subst_list1 ::
    "(nat \<Rightarrow> exp option)
     \<Rightarrow> exp list \<Rightarrow> exp list"
  subst_list2 ::
    "(nat \<Rightarrow> exp option)
     \<Rightarrow> exp list \<Rightarrow> exp list"
### theory "FeatherweightJava.FJDefs"
### 3.338s elapsed time, 5.260s cpu time, 0.344s GC time
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/FeatherweightJava/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/FeatherweightJava/outline -o pdf -n outline -t /proof,/ML
*** Failed to load theory "FeatherweightJava.FJAux" (unresolved "FeatherweightJava.FJDefs")
*** Failed to load theory "FeatherweightJava.FJSound" (unresolved "FeatherweightJava.FJAux")
*** Failed to load theory "FeatherweightJava.Execute" (unresolved "FeatherweightJava.FJSound")
*** Failed to load theory "FeatherweightJava.Featherweight_Java" (unresolved "FeatherweightJava.Execute", "FeatherweightJava.FJSound")
*** Ambiguous input (line 145 of "~~/afp/thys/FeatherweightJava/FJDefs.thy") produces 2 parse trees:
*** ("\<^const>Pure.eq"
***   ("\<^fixed>substs_syn" ("_position" ds) ("_position" xs) ("_position" e))
***   ("_applC" ("_position" substs)
***     ("_cargs"
***       ("_applC" ("_position" map_upds)
***         ("_cargs" ("_position" empty)
***           ("_cargs" ("_position" xs) ("_position" ds))))
***       ("_position" e))))
*** ("\<^const>Pure.eq"
***   ("_applC"
***     ("\<^const>Fields.inverse_class.inverse_divide" ("_position" ds)
***       ("_position" xs))
***     ("_position" e))
***   ("_applC" ("_position" substs)
***     ("_cargs"
***       ("_applC" ("_position" map_upds)
***         ("_cargs" ("_position" empty)
***           ("_cargs" ("_position" xs) ("_position" ds))))
***       ("_position" e))))
*** At command "abbreviation" (line 142 of "~~/afp/thys/FeatherweightJava/FJDefs.thy")
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  map_upds ::
***   (??'a \<Rightarrow> ??'b option)
***   \<Rightarrow> ??'a list
***                 \<Rightarrow> ??'b list
***                               \<Rightarrow> ??'a \<Rightarrow> ??'b option
*** Operand:   {} :: ??'c set
*** 
*** At command "abbreviation" (line 142 of "~~/afp/thys/FeatherweightJava/FJDefs.thy")
*** Type unification failed: No type arity fun :: inverse
*** 
*** Type error in application: operator not of function type
*** 
*** Operator:  ds / xs :: ??'a
*** Operand:   e :: ??'b
*** 
*** At command "abbreviation" (line 142 of "~~/afp/thys/FeatherweightJava/FJDefs.thy")