Loading theory "HOL-Library.Adhoc_Overloading" (required by "Shivers-CFA.AbsCFCorrect")
Loading theory "Shivers-CFA.FixTransform" (required by "Shivers-CFA.AbsCFComp")
signature ADHOC_OVERLOADING =
  sig
    val generic_add_overloaded: string -> Context.generic -> Context.generic
    val generic_add_variant:
       string -> term -> Context.generic -> Context.generic
    val generic_remove_overloaded:
       string -> Context.generic -> Context.generic
    val generic_remove_variant:
       string -> term -> Context.generic -> Context.generic
    val is_overloaded: Proof.context -> string -> bool
    val show_variants: bool Config.T
  end
structure Adhoc_Overloading: ADHOC_OVERLOADING
### theory "HOL-Library.Adhoc_Overloading"
### 0.180s elapsed time, 0.304s cpu time, 0.000s GC time
Loading theory "Shivers-CFA.HOLCFUtils" (required by "Shivers-CFA.Eval")
instantiation
  bool :: po
  below_bool == below :: bool \<Rightarrow> bool \<Rightarrow> bool
instantiation
  set :: (type) po
  below_set == below :: 'a set \<Rightarrow> 'a set \<Rightarrow> bool
### theory "Shivers-CFA.FixTransform"
### 0.255s elapsed time, 0.460s cpu time, 0.000s GC time
Loading theory "Shivers-CFA.CPSScheme" (required by "Shivers-CFA.Eval")
### theory "Shivers-CFA.HOLCFUtils"
### 0.183s elapsed time, 0.372s cpu time, 0.000s GC time
Loading theory "Shivers-CFA.Computability" (required by "Shivers-CFA.AbsCFComp")
### theory "Shivers-CFA.Computability"
### 0.131s elapsed time, 0.264s cpu time, 0.000s GC time
Loading theory "Shivers-CFA.SetMap" (required by "Shivers-CFA.AbsCFCorrect" via "Shivers-CFA.AbsCF")
### Ambiguous input (line 28 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 6 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("_applC"
###     ("\<^fixed>smap_union" ("_position" smap1)
###       ("\<^const>HOL.eq" ("_applC" ("_position" smap2) ("_position" k))
###         ("\<^const>Set.union" ("_applC" ("_position" smap1) ("_position" k))
###           ("_position" smap2))))
###     ("_position" k)))
### ("\<^const>HOL.Trueprop"
###   ("\<^fixed>smap_union" ("_position" smap1)
###     ("\<^const>HOL.eq" ("_applC" ("_position" smap2) ("_position" k))
###       ("\<^const>Set.union" ("_applC" ("_position" smap1) ("_position" k))
###         ("_applC" ("_position" smap2) ("_position" k))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^fixed>smap_union" ("_position" smap1)
###       ("_applC" ("_position" smap2) ("_position" k)))
###     ("\<^const>Set.union" ("_applC" ("_position" smap1) ("_position" k))
###       ("_applC" ("_position" smap2) ("_position" k)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("_applC"
###       ("\<^fixed>smap_union" ("_position" smap1) ("_position" smap2))
###       ("_position" k))
###     ("\<^const>Set.union" ("_applC" ("_position" smap1) ("_position" k))
###       ("_applC" ("_position" smap2) ("_position" k)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.union"
###     ("\<^fixed>smap_union" ("_position" smap1)
###       ("\<^const>HOL.eq" ("_applC" ("_position" smap2) ("_position" k))
###         ("_applC" ("_position" smap1) ("_position" k))))
###     ("_applC" ("_position" smap2) ("_position" k))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>Set.union"
###     ("_applC"
###       ("\<^fixed>smap_union" ("_position" smap1)
###         ("\<^const>HOL.eq" ("_applC" ("_position" smap2) ("_position" k))
###           ("_position" smap1)))
###       ("_position" k))
###     ("_applC" ("_position" smap2) ("_position" k))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 31 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq" ("\<^fixed>smap_Union" ("\<^const>List.list.Nil"))
###     ("\<^const>SetMap.smap_empty")))
### ("\<^const>HOL.Trueprop"
###   ("\<^fixed>smap_Union"
###     ("\<^const>HOL.eq" ("\<^const>List.list.Nil")
###       ("\<^const>SetMap.smap_empty"))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 32 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 5 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^const>HOL.eq"
###       ("\<^fixed>smap_Union"
###         ("\<^const>List.list.Cons" ("_position" m) ("_position" ms)))
###       ("_position" m))
###     ("\<^fixed>smap_Union" ("_position" ms))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^fixed>smap_Union"
###       ("\<^const>HOL.eq"
###         ("\<^const>List.list.Cons" ("_position" m) ("_position" ms))
###         ("_position" m)))
###     ("\<^fixed>smap_Union" ("_position" ms))))
### ("\<^const>HOL.Trueprop"
###   ("\<^fixed>smap_Union"
###     ("\<^const>SetMap.smap_union"
###       ("\<^const>HOL.eq"
###         ("\<^const>List.list.Cons" ("_position" m) ("_position" ms))
###         ("_position" m))
###       ("\<^fixed>smap_Union" ("_position" ms)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^fixed>smap_Union"
###       ("\<^const>List.list.Cons" ("_position" m) ("_position" ms)))
###     ("\<^const>SetMap.smap_union" ("_position" m)
###       ("\<^fixed>smap_Union" ("_position" ms)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^fixed>smap_Union"
###     ("\<^const>HOL.eq"
###       ("\<^const>List.list.Cons" ("_position" m) ("_position" ms))
###       ("\<^const>SetMap.smap_union" ("_position" m)
###         ("\<^fixed>smap_Union" ("_position" ms))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
consts
  smap_Union ::
    "('a \<Rightarrow> 'b set) list \<Rightarrow> 'a \<Rightarrow> 'b set"
### Ignoring duplicate rewrite rule:
### smap_Union [] \<equiv> {}.
### Ambiguous input (line 67 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 5 parse trees:
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>SetMap.smap_less" ("_position" ve1) ("_position" ve1')))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>SetMap.smap_less" ("_position" ve2)
###           ("_position" ve2')))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>SetMap.smap_union"
###       ("\<^const>SetMap.smap_less"
###         ("\<^const>SetMap.smap_union" ("_position" ve1) ("_position" ve2))
###         ("_position" ve1'))
###       ("_position" ve2'))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>SetMap.smap_less" ("_position" ve1) ("_position" ve1')))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>SetMap.smap_less" ("_position" ve2)
###           ("_position" ve2')))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>SetMap.smap_less"
###       ("\<^const>SetMap.smap_union" ("_position" ve1) ("_position" ve2))
###       ("\<^const>SetMap.smap_union" ("_position" ve1')
###         ("_position" ve2')))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>SetMap.smap_less" ("_position" ve1) ("_position" ve1')))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>SetMap.smap_less" ("_position" ve2)
###           ("_position" ve2')))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>SetMap.smap_union" ("_position" ve1)
###       ("\<^const>SetMap.smap_less" ("_position" ve2)
###         ("\<^const>SetMap.smap_union" ("_position" ve1')
###           ("_position" ve2'))))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>SetMap.smap_less" ("_position" ve1) ("_position" ve1')))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>SetMap.smap_less" ("_position" ve2)
###           ("_position" ve2')))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>SetMap.smap_union"
###       ("\<^const>SetMap.smap_union" ("_position" ve1)
###         ("\<^const>SetMap.smap_less" ("_position" ve2) ("_position" ve1')))
###       ("_position" ve2'))))
### ("_bigimpl"
###   ("_asms"
###     ("\<^const>HOL.Trueprop"
###       ("\<^const>SetMap.smap_less" ("_position" ve1) ("_position" ve1')))
###     ("_asm"
###       ("\<^const>HOL.Trueprop"
###         ("\<^const>SetMap.smap_less" ("_position" ve2)
###           ("_position" ve2')))))
###   ("\<^const>HOL.Trueprop"
###     ("\<^const>SetMap.smap_union" ("_position" ve1)
###       ("\<^const>SetMap.smap_union"
###         ("\<^const>SetMap.smap_less" ("_position" ve2) ("_position" ve1'))
###         ("_position" ve2')))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 70 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 3 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union" ("_position" m1)
###     ("\<^const>HOL.eq" ("\<^const>SetMap.smap_Union" ("_position" ms))
###       ("\<^const>SetMap.smap_Union"
###         ("\<^const>List.list.Cons" ("_position" m1) ("_position" ms))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>SetMap.smap_union" ("_position" m1)
###       ("\<^const>SetMap.smap_Union" ("_position" ms)))
###     ("\<^const>SetMap.smap_Union"
###       ("\<^const>List.list.Cons" ("_position" m1) ("_position" ms)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union" ("_position" m1)
###     ("\<^const>SetMap.smap_Union"
###       ("\<^const>HOL.eq" ("_position" ms)
###         ("\<^const>SetMap.smap_Union"
###           ("\<^const>List.list.Cons" ("_position" m1) ("_position" ms)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 75 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_less"
###     ("\<^const>SetMap.smap_Union" ("_position" ms1))
###     ("\<^const>SetMap.smap_Union" ("_position" ms2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_Union"
###     ("\<^const>SetMap.smap_less" ("_position" ms1)
###       ("\<^const>SetMap.smap_Union" ("_position" ms2)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 83 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 5 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^const>HOL.eq"
###       ("\<^const>SetMap.smap_union" ("_position" m1) ("_position" m2))
###       ("_position" m2))
###     ("_position" m1)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^const>SetMap.smap_union" ("_position" m1)
###       ("\<^const>HOL.eq" ("_position" m2) ("_position" m2)))
###     ("_position" m1)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union" ("_position" m1)
###     ("\<^const>SetMap.smap_union"
###       ("\<^const>HOL.eq" ("_position" m2) ("_position" m2))
###       ("_position" m1))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>SetMap.smap_union" ("_position" m1) ("_position" m2))
###     ("\<^const>SetMap.smap_union" ("_position" m2) ("_position" m1))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union" ("_position" m1)
###     ("\<^const>HOL.eq" ("_position" m2)
###       ("\<^const>SetMap.smap_union" ("_position" m2) ("_position" m1)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 86 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>SetMap.smap_union" ("\<^const>SetMap.smap_empty")
###       ("_position" m))
###     ("_position" m)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union" ("\<^const>SetMap.smap_empty")
###     ("\<^const>HOL.eq" ("_position" m) ("_position" m))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 89 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>SetMap.smap_union" ("_position" m)
###       ("\<^const>SetMap.smap_empty"))
###     ("_position" m)))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union" ("_position" m)
###     ("\<^const>HOL.eq" ("\<^const>SetMap.smap_empty") ("_position" m))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 92 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 5 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^const>HOL.eq"
###       ("\<^const>SetMap.smap_union"
###         ("\<^const>SetMap.smap_union" ("_position" m1) ("_position" m2))
###         ("_position" m3))
###       ("_position" m1))
###     ("\<^const>SetMap.smap_union" ("_position" m2) ("_position" m3))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^const>SetMap.smap_union"
###       ("\<^const>SetMap.smap_union" ("_position" m1) ("_position" m2))
###       ("\<^const>HOL.eq" ("_position" m3) ("_position" m1)))
###     ("\<^const>SetMap.smap_union" ("_position" m2) ("_position" m3))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^const>SetMap.smap_union" ("_position" m1) ("_position" m2))
###     ("\<^const>SetMap.smap_union"
###       ("\<^const>HOL.eq" ("_position" m3) ("_position" m1))
###       ("\<^const>SetMap.smap_union" ("_position" m2) ("_position" m3)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>SetMap.smap_union"
###       ("\<^const>SetMap.smap_union" ("_position" m1) ("_position" m2))
###       ("_position" m3))
###     ("\<^const>SetMap.smap_union" ("_position" m1)
###       ("\<^const>SetMap.smap_union" ("_position" m2) ("_position" m3)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^const>SetMap.smap_union" ("_position" m1) ("_position" m2))
###     ("\<^const>HOL.eq" ("_position" m3)
###       ("\<^const>SetMap.smap_union" ("_position" m1)
###         ("\<^const>SetMap.smap_union" ("_position" m2) ("_position" m3))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 95 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 5 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^const>HOL.eq"
###       ("\<^const>SetMap.smap_Union"
###         ("\<^const>List.append" ("_position" m1) ("_position" m2)))
###       ("\<^const>SetMap.smap_Union" ("_position" m1)))
###     ("\<^const>SetMap.smap_Union" ("_position" m2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_union"
###     ("\<^const>SetMap.smap_Union"
###       ("\<^const>HOL.eq"
###         ("\<^const>List.append" ("_position" m1) ("_position" m2))
###         ("\<^const>SetMap.smap_Union" ("_position" m1))))
###     ("\<^const>SetMap.smap_Union" ("_position" m2))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_Union"
###     ("\<^const>SetMap.smap_union"
###       ("\<^const>HOL.eq"
###         ("\<^const>List.append" ("_position" m1) ("_position" m2))
###         ("\<^const>SetMap.smap_Union" ("_position" m1)))
###       ("\<^const>SetMap.smap_Union" ("_position" m2)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>SetMap.smap_Union"
###       ("\<^const>List.append" ("_position" m1) ("_position" m2)))
###     ("\<^const>SetMap.smap_union"
###       ("\<^const>SetMap.smap_Union" ("_position" m1))
###       ("\<^const>SetMap.smap_Union" ("_position" m2)))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_Union"
###     ("\<^const>HOL.eq"
###       ("\<^const>List.append" ("_position" m1) ("_position" m2))
###       ("\<^const>SetMap.smap_union"
###         ("\<^const>SetMap.smap_Union" ("_position" m1))
###         ("\<^const>SetMap.smap_Union" ("_position" m2))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 98 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>SetMap.smap_Union"
###       ("_applC" ("_position" rev) ("_position" l)))
###     ("\<^const>SetMap.smap_Union" ("_position" l))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_Union"
###     ("\<^const>HOL.eq" ("_applC" ("_position" rev) ("_position" l))
###       ("\<^const>SetMap.smap_Union" ("_position" l)))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### Ambiguous input (line 101 of "~~/afp/thys/Shivers-CFA/SetMap.thy") produces 2 parse trees:
### ("\<^const>HOL.Trueprop"
###   ("\<^const>HOL.eq"
###     ("\<^const>SetMap.smap_Union"
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" f)
###           ("_applC" ("_position" rev) ("_position" l)))))
###     ("\<^const>SetMap.smap_Union"
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" f) ("_position" l))))))
### ("\<^const>HOL.Trueprop"
###   ("\<^const>SetMap.smap_Union"
###     ("\<^const>HOL.eq"
###       ("_applC" ("_position" map)
###         ("_cargs" ("_position" f)
###           ("_applC" ("_position" rev) ("_position" l))))
###       ("\<^const>SetMap.smap_Union"
###         ("_applC" ("_position" map)
###           ("_cargs" ("_position" f) ("_position" l)))))))
### Fortunately, only one parse tree is well-formed and type-correct,
### but you may still want to disambiguate your grammar or your input.
### theory "Shivers-CFA.SetMap"
### 0.214s elapsed time, 0.416s cpu time, 0.000s GC time
Loading theory "Shivers-CFA.Utils" (required by "Shivers-CFA.AbsCFCorrect" via "Shivers-CFA.AbsCF")
### Ignoring duplicate rewrite rule:
### single_valued {} \<equiv> True
### theory "Shivers-CFA.Utils"
### 0.123s elapsed time, 0.124s cpu time, 0.000s GC time
Loading theory "Shivers-CFA.MapSets" (required by "Shivers-CFA.AbsCFComp")
### theory "Shivers-CFA.MapSets"
### 0.169s elapsed time, 0.336s cpu time, 0.000s GC time
### Ignoring duplicate rewrite rule:
### (\<And>y. cont (\<lambda>x. ?f1 x y)) \<Longrightarrow>
### cont ?f1 \<equiv> True
### theory "Shivers-CFA.CPSScheme"
### 9.631s elapsed time, 17.956s cpu time, 1.072s GC time
Loading theory "Shivers-CFA.CPSUtils" (required by "Shivers-CFA.AbsCFComp")
Found termination order: "case_sum size (case_sum size size) <*mlex*> {}"
Found termination order: "case_sum size (case_sum size size) <*mlex*> {}"
Found termination order: "case_sum size (case_sum size size) <*mlex*> {}"
Found termination order: "{}"
Found termination order: "case_sum size (case_sum size size) <*mlex*> {}"
Found termination order: "case_sum size (case_sum size size) <*mlex*> {}"
Found termination order: "case_sum size (case_sum size size) <*mlex*> {}"
### theory "Shivers-CFA.CPSUtils"
### 2.297s elapsed time, 4.512s cpu time, 0.272s GC time
Loading theory "Shivers-CFA.Eval"
Loading theory "Shivers-CFA.AbsCF" (required by "Shivers-CFA.AbsCFCorrect")
Found termination order: "{}"
class contour = finite +
  fixes nb_a :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
    and a_initial_contour :: "'a"
instantiation
  unit :: contour
  nb_a_unit == nb_a :: unit \<Rightarrow> nat \<Rightarrow> unit
  a_initial_contour_unit == a_initial_contour :: unit
### theory "Shivers-CFA.Eval"
### 1.494s elapsed time, 2.976s cpu time, 0.000s GC time
Loading theory "Shivers-CFA.ExCF" (required by "Shivers-CFA.AbsCFCorrect")
instantiation
  contour :: preorder
  less_eq_contour == less_eq ::
    contour \<Rightarrow> contour \<Rightarrow> bool
  less_contour == less :: contour \<Rightarrow> contour \<Rightarrow> bool
Found termination order: "{}"
consts
  isProc :: "d \<Rightarrow> bool"
instantiation
  contour :: discrete_cpo
  below_contour == below :: contour \<Rightarrow> contour \<Rightarrow> bool
instantiation
  d :: discrete_cpo
  below_d == below :: d \<Rightarrow> d \<Rightarrow> bool
instantiation
  call :: discrete_cpo
  below_call == below :: call \<Rightarrow> call \<Rightarrow> bool
Found termination order: "{}"
### Missing patterns in function definition:
### \<And>va vb c d. a_evalF_cases (PP (prim.If va vb)) [] c d = undefined
### \<And>va vb v c d. a_evalF_cases (PP (prim.If va vb)) [v] c d = undefined
### \<And>va vb v vd c d.
###    a_evalF_cases (PP (prim.If va vb)) [v, vd] c d = undefined
### (7 more)
### theory "Shivers-CFA.ExCF"
### 2.065s elapsed time, 3.952s cpu time, 0.392s GC time
Found termination order: "{}"
### theory "Shivers-CFA.AbsCF"
### 3.517s elapsed time, 6.840s cpu time, 0.392s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/document -o pdf -n document
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/outline -o pdf -n outline -t /proof,/ML
*** Failed to load theory "Shivers-CFA.ExCFSV" (unresolved "Shivers-CFA.ExCF")
*** Failed to load theory "Shivers-CFA.AbsCFCorrect" (unresolved "Shivers-CFA.AbsCF", "Shivers-CFA.ExCF")
*** Failed to load theory "Shivers-CFA.AbsCFComp" (unresolved "Shivers-CFA.AbsCF", "Shivers-CFA.MapSets")
*** Latex error:
***   File `ExCFSV.tex' not found.
*** Latex error (line 61 of "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/document/root.tex"):
***   Emergency stop.
***   <read *> 
***            
***   \input{ExCFSV}
*** Latex error (line 61 of "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/document/root.tex"):
***    ==> Fatal error occurred, no output PDF file produced!
*** Failed to build document in "/media/data/jenkins/workspace/isabelle-repo-afp/browser_info/AFP/Shivers-CFA/document"
*** Type unification failed: Clash of types "_ \<Rightarrow> _" and "_ set"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  HOL.Let {} :: (??'a set \<Rightarrow> ??'b) \<Rightarrow> ??'b
*** Operand:
***   \<lambda>\<beta>.
***      let f = \<aA> (L l) \<beta> ve
***      in \<aF>\<cdot>(Discr (the_elem f, [{AStop}], ve, \<abinit>)) ::
***   (nat \<Rightarrow> ??'c option)
***   \<Rightarrow> ((nat \<times> (nat \<Rightarrow> ??'c option)) \<times>
***                  ??'c \<aproc>) set
*** 
*** At command "definition" (line 180 of "~~/afp/thys/Shivers-CFA/AbsCF.thy")
*** Type unification failed: Clash of types "_ \<Rightarrow> _" and "_ set"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  HOL.Let {} :: (??'a set \<Rightarrow> ??'b) \<Rightarrow> ??'b
*** Operand:
***   \<lambda>\<beta>.
***      let f = \<A> (L l) \<beta> ve
***      in \<F>\<cdot>(Discr (f, [Stop], ve, \<binit>)) ::
***   (nat \<Rightarrow> contour option)
***   \<Rightarrow> ((nat \<times> (nat \<Rightarrow> contour option)) \<times>
***                  d) set
*** 
*** At command "definition" (line 231 of "~~/afp/thys/Shivers-CFA/ExCF.thy")
*** Type unification failed: Clash of types "_ \<Rightarrow> _" and "_ set"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  HOL.Let {} :: (??'a set \<Rightarrow> ??'b) \<Rightarrow> ??'b
*** Operand:
***   \<lambda>\<beta>.
***      let f = \<A> (L l) \<beta> ve
***      in \<F>\<cdot>(Discr (f, [Stop], ve, 0)) ::
***   (nat \<Rightarrow> nat option) \<Rightarrow> int lift
*** 
*** At command "definition" (line 137 of "~~/afp/thys/Shivers-CFA/Eval.thy")
*** Type unification failed: Clash of types "_ \<Rightarrow> _" and "_ set"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  (\<in>) {} :: ??'a set set \<Rightarrow> bool
*** Operand:   maps_over A B :: (??'b \<Rightarrow> ??'c option) set
*** 
*** At command "lemma" (line 13 of "~~/afp/thys/Shivers-CFA/MapSets.thy")