Loading theory "HOL-Library.Old_Datatype" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOL-Library.Countable")
Loading theory "HOL-Library.Nat_Bijection" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOL-Library.Countable")
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
### theory "HOL-Library.Nat_Bijection"
### 0.594s elapsed time, 1.248s cpu time, 0.000s GC time
Loading theory "HOLCF.Porder" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Deflation" via "HOLCF.Cfun" via "HOLCF.Cpodef" via "HOLCF.Adm" via "HOLCF.Cont" via "HOLCF.Pcpo")
class below = type +
  fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
class po = below +
  assumes "below_refl": "\<And>x. x \<sqsubseteq> x"
  assumes
    "below_trans":
      "\<And>x y z.
          \<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk>
          \<Longrightarrow> x \<sqsubseteq> z"
  assumes
    "below_antisym":
      "\<And>x y.
          \<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk>
          \<Longrightarrow> x = y"
class po = below +
  assumes "below_refl": "\<And>x. x \<sqsubseteq> x"
  assumes
    "below_trans":
      "\<And>x y z.
          \<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk>
          \<Longrightarrow> x \<sqsubseteq> z"
  assumes
    "below_antisym":
      "\<And>x y.
          \<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk>
          \<Longrightarrow> x = y"
signature OLD_DATATYPE =
  sig
    val check_specs: spec list -> theory -> spec list * Proof.context
    type config = {quiet: bool, strict: bool}
    val default_config: config
    type descr =
       (int * (string * dtyp list * (string * dtyp list) list)) list
    val distinct_lemma: thm
    datatype dtyp
    = DtRec of int | DtTFree of string * sort | DtType of string * dtyp list
    type info =
       {case_cong: thm,
        case_cong_weak: thm,
        case_name: string,
        case_rewrites: thm list,
        descr: descr,
        distinct: thm list,
        exhaust: thm,
        index: int,
        induct: thm,
        inducts: thm list,
        inject: thm list,
        nchotomy: thm,
        rec_names: string list,
        rec_rewrites: thm list, split: thm, split_asm: thm}
    val read_specs: spec_cmd list -> theory -> spec list * Proof.context
    type spec =
       (binding * (string * sort) list * mixfix) *
       (binding * typ list * mixfix) list
    type spec_cmd =
       (binding * (string * string option) list * mixfix) *
       (binding * string list * mixfix) list
  end
structure Old_Datatype: OLD_DATATYPE
### theory "HOL-Library.Old_Datatype"
### 0.796s elapsed time, 1.644s cpu time, 0.000s GC time
Loading theory "HOL-Library.Countable" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite")
class po = below +
  assumes "below_refl": "\<And>x. x \<sqsubseteq> x"
  assumes
    "below_trans":
      "\<And>x y z.
          \<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk>
          \<Longrightarrow> x \<sqsubseteq> z"
  assumes
    "below_antisym":
      "\<And>x y.
          \<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk>
          \<Longrightarrow> x = y"
### theory "HOLCF.Porder"
### 0.474s elapsed time, 0.940s cpu time, 0.000s GC time
Loading theory "HOLCF.Pcpo" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Deflation" via "HOLCF.Cfun" via "HOLCF.Cpodef" via "HOLCF.Adm" via "HOLCF.Cont")
class cpo = po +
  assumes
    "cpo": "\<And>S. chain S \<Longrightarrow> \<exists>x. range S <<| x"
### Additional type variable(s) in locale specification "countable": 'a
class pcpo = cpo +
  assumes "least": "\<exists>x. \<forall>y. x \<sqsubseteq> y"
class countable = type +
  assumes "ex_inj": "\<exists>to_nat. inj to_nat"
class chfin = po +
  assumes
    "chfin":
      "\<And>Y. chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
Proofs for inductive predicate(s) "finite_item"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the induction rule ...
  Proving the simplification rules ...
class flat = pcpo +
  assumes
    "ax_flat":
      "\<And>x y.
          x \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
val old_countable_datatype_tac = fn: Proof.context -> int -> tactic
class discrete_cpo = below +
  assumes "discrete_cpo": "\<And>x y. (x \<sqsubseteq> y) = (x = y)"
### ML warning (line 93 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"):
### Pattern is not exhaustive.
### ML warning (line 139 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"):
### Pattern is not exhaustive.
### ML warning (line 143 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"):
### Matches are not exhaustive.
### ML warning (line 145 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"):
### Matches are not exhaustive.
### ML warning (line 156 of "~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML"):
### Pattern is not exhaustive.
signature BNF_LFP_COUNTABLE =
  sig
    val countable_datatype_tac: Proof.context -> tactic
    val derive_encode_injectives_thms:
       Proof.context -> string list -> thm list
  end
structure BNF_LFP_Countable: BNF_LFP_COUNTABLE
val countable_datatype_tac = fn: Proof.context -> thm -> thm Seq.seq
val countable_tac = fn: Proof.context -> int -> tactic
### theory "HOLCF.Pcpo"
### 1.433s elapsed time, 2.800s cpu time, 0.380s GC time
Loading theory "HOLCF.Cont" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Deflation" via "HOLCF.Cfun" via "HOLCF.Cpodef" via "HOLCF.Adm")
### theory "HOL-Library.Countable"
### 1.757s elapsed time, 3.440s cpu time, 0.380s GC time
### theory "HOLCF.Cont"
### 0.299s elapsed time, 0.596s cpu time, 0.000s GC time
Loading theory "HOLCF.Adm" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Deflation" via "HOLCF.Cfun" via "HOLCF.Cpodef")
Loading theory "HOLCF.Discrete" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Ssum" via "HOLCF.Tr" via "HOLCF.Lift")
### theory "HOLCF.Adm"
### 0.173s elapsed time, 0.348s cpu time, 0.000s GC time
Loading theory "HOLCF.Cpodef" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Deflation" via "HOLCF.Cfun")
### ML warning (line 143 of "~~/src/HOL/HOLCF/Tools/cpodef.ML"):
### Value identifier (name) has not been referenced.
signature CPODEF =
  sig
    val add_cpodef:
       binding * (string * sort) list * mixfix ->
         term ->
           Typedef.bindings option ->
             (Proof.context -> tactic) * (Proof.context -> tactic) ->
               theory -> (Typedef.info * cpo_info) * theory
    val add_pcpodef:
       binding * (string * sort) list * mixfix ->
         term ->
           Typedef.bindings option ->
             (Proof.context -> tactic) * (Proof.context -> tactic) ->
               theory -> (Typedef.info * cpo_info * pcpo_info) * theory
    val add_podef:
       binding * (string * sort) list * mixfix ->
         term ->
           Typedef.bindings option ->
             (Proof.context -> tactic) ->
               theory -> (Typedef.info * thm) * theory
    type cpo_info =
       {adm: thm,
        below_def: thm,
        compact: thm, cont_Abs: thm, cont_Rep: thm, lub: thm}
    val cpodef_proof:
       (binding * (string * sort) list * mixfix) * term *
       Typedef.bindings option
         -> theory -> Proof.state
    val cpodef_proof_cmd:
       (binding * (string * string option) list * mixfix) * string *
       Typedef.bindings option
         -> theory -> Proof.state
    type pcpo_info =
       {Abs_bottom_iff: thm,
        Abs_strict: thm, Rep_bottom_iff: thm, Rep_strict: thm}
    val pcpodef_proof:
       (binding * (string * sort) list * mixfix) * term *
       Typedef.bindings option
         -> theory -> Proof.state
    val pcpodef_proof_cmd:
       (binding * (string * string option) list * mixfix) * string *
       Typedef.bindings option
         -> theory -> Proof.state
  end
structure Cpodef: CPODEF
### theory "HOLCF.Cpodef"
### 0.245s elapsed time, 0.492s cpu time, 0.000s GC time
Loading theory "HOLCF.Fun_Cpo" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Deflation" via "HOLCF.Cfun")
instantiation
  fun :: (type, below) below
  below_fun == below ::
    ('a \<Rightarrow> 'b)
    \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool
### theory "HOLCF.Fun_Cpo"
### 0.088s elapsed time, 0.176s cpu time, 0.000s GC time
Loading theory "HOLCF.Product_Cpo" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Deflation" via "HOLCF.Cfun")
instantiation
  unit :: discrete_cpo
  below_unit == below :: unit \<Rightarrow> unit \<Rightarrow> bool
instantiation
  discr :: (type) discrete_cpo
  below_discr == below :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool
instantiation
  prod :: (below, below) below
  below_prod == below ::
    'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool
### theory "HOLCF.Discrete"
### 0.567s elapsed time, 1.132s cpu time, 0.000s GC time
### theory "HOLCF.Product_Cpo"
### 0.190s elapsed time, 0.380s cpu time, 0.000s GC time
Loading theory "HOLCF.Cfun" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Deflation")
### theory "HOLCF.Cfun"
### 0.733s elapsed time, 1.460s cpu time, 0.000s GC time
Loading theory "HOLCF.Completion" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal")
Loading theory "HOLCF.Cprod" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite")
locale Completion.preorder
  fixes
    r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix "\<preceq>" 50)
  assumes "preorder (\<preceq>)"
### theory "HOLCF.Cprod"
### 0.073s elapsed time, 0.144s cpu time, 0.000s GC time
Loading theory "HOLCF.Deflation" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions")
locale deflation
  fixes d :: "'a \<rightarrow> 'a" 
  assumes "deflation d"
locale ideal_completion
  fixes
    r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"   (infix "\<preceq>" 50)
    and principal :: "'a \<Rightarrow> 'b" 
    and rep :: "'b \<Rightarrow> 'a set" 
  assumes "ideal_completion (\<preceq>) principal rep"
locale finite_deflation
  fixes d :: "'a \<rightarrow> 'a" 
  assumes "finite_deflation d"
locale ep_pair
  fixes e :: "'a \<rightarrow> 'b" 
    and p :: "'b \<rightarrow> 'a" 
  assumes "ep_pair e p"
### theory "HOLCF.Completion"
### 0.298s elapsed time, 0.592s cpu time, 0.000s GC time
Loading theory "HOLCF.Fix" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Domain_Aux" via "HOLCF.Fixrec")
locale pcpo_ep_pair
  fixes e :: "'a \<rightarrow> 'b" 
    and p :: "'b \<rightarrow> 'a" 
  assumes "pcpo_ep_pair e p"
### theory "HOLCF.Deflation"
### 0.241s elapsed time, 0.480s cpu time, 0.000s GC time
Loading theory "HOLCF.Sfun" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions")
consts
  iterate ::
    "nat
     \<Rightarrow> ('a \<rightarrow> 'a) \<rightarrow> 'a \<rightarrow> 'a"
### theory "HOLCF.Sfun"
### 0.140s elapsed time, 0.280s cpu time, 0.000s GC time
Loading theory "HOLCF.Sprod" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions")
### theory "HOLCF.Fix"
### 0.208s elapsed time, 0.416s cpu time, 0.000s GC time
Loading theory "HOLCF.Up" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Ssum" via "HOLCF.Tr" via "HOLCF.Lift")
### theory "HOLCF.Sprod"
### 0.319s elapsed time, 0.636s cpu time, 0.000s GC time
consts
  Ifup ::
    "('a \<rightarrow> 'b)
     \<Rightarrow> 'a\<^sub>\<bottom> \<Rightarrow> 'b"
instantiation
  u :: (cpo) below
  below_u == below ::
    'a\<^sub>\<bottom> \<Rightarrow> 'a\<^sub>\<bottom> \<Rightarrow> bool
### theory "HOLCF.Up"
### 0.848s elapsed time, 1.680s cpu time, 0.000s GC time
Loading theory "HOLCF.Lift" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Ssum" via "HOLCF.Tr")
Proofs for inductive predicate(s) "rec_set_lift"
  Proving monotonicity ...
  Proving the introduction rules ...
  Proving the elimination rules ...
  Proving the simplification rules ...
### theory "HOLCF.Lift"
### 0.808s elapsed time, 1.584s cpu time, 0.580s GC time
Loading theory "HOLCF.One" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Domain_Aux" via "HOLCF.Fixrec")
Loading theory "HOLCF.Tr" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions" via "HOLCF.Ssum")
### theory "HOLCF.One"
### 0.075s elapsed time, 0.148s cpu time, 0.000s GC time
### Introduced fixed type variable(s): 'd in "y__"
val split_If_tac = fn: Proof.context -> int -> tactic
### theory "HOLCF.Tr"
### 0.181s elapsed time, 0.364s cpu time, 0.000s GC time
Loading theory "HOLCF.Ssum" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite" via "HOLCF.Map_Functions")
### theory "HOLCF.Ssum"
### 0.268s elapsed time, 0.532s cpu time, 0.000s GC time
Loading theory "HOLCF.Fixrec" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Domain_Aux")
Loading theory "HOLCF.Map_Functions" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal" via "HOLCF.Bifinite")
### theory "HOLCF.Map_Functions"
### 0.955s elapsed time, 1.912s cpu time, 0.000s GC time
Loading theory "HOLCF.Bifinite" (required by "HOLCF" via "HOLCF.Domain" via "HOLCF.Representable" via "HOLCF.Algebraic" via "HOLCF.Universal")
structure HOLCF_Library:
  sig
    val -->> : typ list * typ -> typ
    val ->> : typ * typ -> typ
    val ` : term * term -> term
    val below_const: typ -> term
    val big_lambda: term -> term -> term
    val big_lambdas: term list -> term -> term
    val boolT: typ
    val cabs_const: typ * typ -> term
    val capply_const: typ * typ -> term
    val cfcomp_const: typ * typ * typ -> term
    val dest_cfunT: typ -> typ * typ
    val dest_matchT: typ -> typ
    val dest_sprodT: typ -> typ * typ
    val dest_ssumT: typ -> typ * typ
    val dest_upT: typ -> typ
    val from_sinl: typ * typ -> term
    val from_sinr: typ * typ -> term
    val from_up: typ -> term
    val fup_const: typ * typ -> term
    val iterate_const: typ -> term
    val lambda_tuple: term list -> term -> term
    val lambdas: term list -> term -> term
    val list_ccomb: term * term list -> term
    val mk_ID: typ -> term
    val mk_adm: term -> term
    val mk_all: term * term -> term
    val mk_below: term * term -> term
    val mk_bottom: typ -> term
    val mk_cabs: term -> term
    val mk_capply: term * term -> term
    val mk_cfcomp: term * term -> term
    val mk_cfunT: typ * typ -> typ
    val mk_chain: term -> term
    val mk_compact: term -> term
    val mk_conj: term * term -> term
    val mk_cont: term -> term
    val mk_defined: term -> term
    val mk_disj: term * term -> term
    val mk_eq: term * term -> term
    val mk_equals: term * term -> term
    val mk_ex: term * term -> term
    val mk_fail: typ -> term
    val mk_fix: term -> term
    val mk_fst: term -> term
    val mk_fup: term -> term
    val mk_imp: term * term -> term
    val mk_iterate: term * term -> term
    val mk_lub: term -> term
    val mk_matchT: typ -> typ
    val mk_not: term -> term
    val mk_one_case: term -> term
    val mk_prodT: typ * typ -> typ
    val mk_setT: typ -> typ
    val mk_sinjects: term list -> term list
    val mk_snd: term -> term
    val mk_spair: term * term -> term
    val mk_sprodT: typ * typ -> typ
    val mk_sscase: term * term -> term
    val mk_ssplit: term -> term
    val mk_ssumT: typ * typ -> typ
    val mk_strict: term -> term
    val mk_strictify: term -> term
    val mk_stuple: term list -> term
    val mk_succeed: term -> term
    val mk_trp: term -> term
    val mk_tuple: term list -> term
    val mk_tupleT: typ list -> typ
    val mk_undef: term -> term
    val mk_up: term -> term
    val mk_upT: typ -> typ
    val natT: typ
    val oneT: typ
    val one_case_const: typ -> term
    val sfst_const: typ * typ -> term
    val sinl_const: typ * typ -> term
    val sinr_const: typ * typ -> term
    val spair_const: typ * typ -> term
    val sscase_const: typ * typ * typ -> term
    val ssnd_const: typ * typ -> term
    val ssplit_const: typ * typ * typ -> term
    val strictify_const: typ -> term
    val succeed_const: typ -> term
    val trT: typ
    val up_const: typ -> term
  end
signature FIXREC =
  sig
    val add_fixrec:
       (binding * typ option * mixfix) list ->
         (bool * (Attrib.binding * term)) list ->
           local_theory -> local_theory
    val add_fixrec_cmd:
       (binding * string option * mixfix) list ->
         (bool * (Attrib.binding * string)) list ->
           local_theory -> local_theory
    val add_matchers: (string * string) list -> theory -> theory
    val fixrec_simp_tac: Proof.context -> int -> tactic
  end
structure Fixrec: FIXREC
### theory "HOLCF.Fixrec"
### 1.287s elapsed time, 2.572s cpu time, 0.000s GC time
Loading theory "HOLCF.Domain_Aux" (required by "HOLCF" via "HOLCF.Domain")
locale iso
  fixes abs :: "'a \<rightarrow> 'b" 
    and rep :: "'b \<rightarrow> 'a" 
  assumes "Domain_Aux.iso abs rep"
locale approx_chain
  fixes approx :: "nat \<Rightarrow> 'a \<rightarrow> 'a" 
  assumes "approx_chain approx"
### theory "HOLCF.Bifinite"
### 0.536s elapsed time, 1.068s cpu time, 0.000s GC time
signature DOMAIN_TAKE_PROOFS =
  sig
    val add_deflation_thm: thm -> theory -> theory
    val add_lub_take_theorems:
       (binding * iso_info) list ->
         take_info -> thm list -> theory -> take_induct_info * theory
    val add_rec_type: string * bool list -> theory -> theory
    val define_take_functions:
       (binding * iso_info) list -> theory -> take_info * theory
    val get_deflation_thms: theory -> thm list
    val get_map_ID_thms: theory -> thm list
    val get_rec_tab: theory -> bool list Symtab.table
    type iso_info =
       {absT: typ,
        abs_const: term,
        abs_inverse: thm, repT: typ, rep_const: term, rep_inverse: thm}
    val map_ID_add: attribute
    val map_of_typ: theory -> (typ * term) list -> typ -> term
    type take_induct_info =
       {chain_take_thms: thm list,
        deflation_take_thms: thm list,
        finite_consts: term list,
        finite_defs: thm list,
        is_finite: bool,
        lub_take_thms: thm list,
        reach_thms: thm list,
        take_0_thms: thm list,
        take_Suc_thms: thm list,
        take_consts: term list,
        take_defs: thm list,
        take_induct_thms: thm list,
        take_lemma_thms: thm list, take_strict_thms: thm list}
    type take_info =
       {chain_take_thms: thm list,
        deflation_take_thms: thm list,
        finite_consts: term list,
        finite_defs: thm list,
        take_0_thms: thm list,
        take_Suc_thms: thm list,
        take_consts: term list,
        take_defs: thm list, take_strict_thms: thm list}
  end
structure Domain_Take_Proofs: DOMAIN_TAKE_PROOFS
signature CONT_CONSTS =
  sig
    val add_consts: (binding * typ * mixfix) list -> theory -> theory
    val add_consts_cmd: (binding * string * mixfix) list -> theory -> theory
  end
structure Cont_Consts: CONT_CONSTS
signature CONT_PROC =
  sig
    val all_cont_thms: term -> thm list
    val cont_proc: simproc
    val cont_tac: Proof.context -> int -> tactic
    val cont_thms: term -> thm list
    val is_lcf_term: term -> bool
    val setup: theory -> theory
  end
structure ContProc: CONT_PROC
### Ignoring duplicate rewrite rule:
### \<forall>x\<in>?A1. ?P1 x \<or> ?Q1 \<equiv>
### (\<forall>x\<in>?A1. ?P1 x) \<or> ?Q1
### Ignoring duplicate rewrite rule:
### \<forall>x\<in>?A1. ?P1 \<or> ?Q1 x \<equiv>
### ?P1 \<or> (\<forall>x\<in>?A1. ?Q1 x)
### Ignoring duplicate rewrite rule:
### \<forall>x\<in>?A1. ?P1 \<longrightarrow> ?Q1 x \<equiv>
### ?P1 \<longrightarrow> (\<forall>x\<in>?A1. ?Q1 x)
### Ignoring duplicate rewrite rule:
### \<forall>x\<in>?A1. ?P1 x \<longrightarrow> ?Q1 \<equiv>
### (\<exists>x\<in>?A1. ?P1 x) \<longrightarrow> ?Q1
### Ignoring duplicate rewrite rule:
### \<forall>x\<in>{}. ?P1 x \<equiv> True
### Ignoring duplicate rewrite rule:
### \<forall>x\<in>UNIV. ?P1 x \<equiv> \<forall>x. ?P1 x
### Ignoring duplicate rewrite rule:
### \<forall>x\<in>insert ?a1 ?B1. ?P1 x \<equiv>
### ?P1 ?a1 \<and> (\<forall>x\<in>?B1. ?P1 x)
### Ignoring duplicate rewrite rule:
### \<forall>x\<in>Collect ?Q1. ?P1 x \<equiv>
### \<forall>x. ?Q1 x \<longrightarrow> ?P1 x
### Ignoring duplicate rewrite rule:
### \<forall>x\<in>?f1 ` ?A1. ?P1 x \<equiv> \<forall>x\<in>?A1. ?P1 (?f1 x)
### Ignoring duplicate rewrite rule:
### \<not> (\<forall>x\<in>?A1. ?P1 x) \<equiv> \<exists>x\<in>?A1. \<not> ?P1 x
signature DOMAIN_CONSTRUCTORS =
  sig
    val add_domain_constructors:
       binding ->
         (binding * (bool * binding option * typ) list * mixfix) list ->
           Domain_Take_Proofs.iso_info -> theory -> constr_info * theory
    type constr_info =
       {cases: thm list,
        compacts: thm list,
        con_betas: thm list,
        con_rews: thm list,
        con_specs: (term * (bool * typ) list) list,
        dis_rews: thm list,
        dist_eqs: thm list,
        dist_les: thm list,
        exhaust: thm,
        injects: thm list,
        inverts: thm list,
        iso_info: Domain_Take_Proofs.iso_info,
        match_rews: thm list, nchotomy: thm, sel_rews: thm list}
  end
structure Domain_Constructors: DOMAIN_CONSTRUCTORS
signature DOMAIN_INDUCTION =
  sig
    val comp_theorems:
       binding list ->
         Domain_Take_Proofs.take_induct_info ->
           Domain_Constructors.constr_info list ->
             theory -> thm list * theory
    val quiet_mode: bool ref
    val trace_domain: bool ref
  end
structure Domain_Induction: DOMAIN_INDUCTION
### theory "HOLCF.Domain_Aux"
### 1.830s elapsed time, 3.628s cpu time, 0.608s GC time
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/isabelle-repo-makeall/browser_info/HOL/HOLCF/document -o pdf -n document
*** Failed to load theory "HOLCF.Universal" (unresolved "HOLCF.Bifinite")
*** Failed to load theory "HOLCF.Algebraic" (unresolved "HOLCF.Universal")
*** Failed to load theory "HOLCF.Compact_Basis" (unresolved "HOLCF.Universal")
*** Failed to load theory "HOLCF.LowerPD" (unresolved "HOLCF.Compact_Basis")
*** Failed to load theory "HOLCF.UpperPD" (unresolved "HOLCF.Compact_Basis")
*** Failed to load theory "HOLCF.ConvexPD" (unresolved "HOLCF.LowerPD", "HOLCF.UpperPD")
*** Failed to load theory "HOLCF.Representable" (unresolved "HOLCF.Algebraic")
*** Failed to load theory "HOLCF.Domain" (unresolved "HOLCF.Representable")
*** Failed to load theory "HOLCF.Powerdomains" (unresolved "HOLCF.ConvexPD", "HOLCF.Domain")
*** Failed to load theory "HOLCF" (unresolved "HOLCF.Domain", "HOLCF.Powerdomains")
*** Type unification failed: Variable 'a::type not of sort cpo
*** 
*** Failed to meet type constraint:
*** 
*** Term:  approx_chain ::
***   (nat \<Rightarrow> ??'b \<rightarrow> ??'b) \<Rightarrow> bool
*** Type:  (nat \<Rightarrow> 'a \<rightarrow> 'a) \<Rightarrow> ??'a
*** 
*** At command "class" (line 48 of "~~/src/HOL/HOLCF/Bifinite.thy")