theory type_class_sidekick_helper 
imports Complex_Main 
begin

section{*all: import BNF Complex_Main 2013-2*}

subsection{*N-82, Z-106, Q-110, R-143, C-88*}

print_classes

subsection{*N,Z,_,_,_: Gcd*}
  term "x::'a::Gcd"
  print_locale Gcd
  print_dependencies Gcd (*
class Gcd
  supersort: gcd
  parameters:
    Gcd :: ('a set \<Rightarrow> 'a)
    Lcm :: ('a set \<Rightarrow> 'a)
  instances:
    int :: Gcd
    nat :: Gcd *)

subsection{*_,_,_,R,_: Inf*}
  term "x::'a::Inf"
  print_locale Inf
  print_dependencies Inf (*
class Inf
  supersort: type
  parameters:
    Inf :: ('a set \<Rightarrow> 'a)
  instances:
    Predicate.pred :: (type) Inf
    bool :: Inf
    filter :: (type) Inf
    fset :: (type) Inf
    fun :: (type, complete_lattice) Inf
    real :: Inf
    set :: (type) Inf *)

subsection{*_,_,_,R,_: Sup*}
  term "x::'a::Sup"
  print_locale Sup
  print_dependencies Sup (*
class Sup
  supersort: type
  parameters:
    Sup :: ('a set \<Rightarrow> 'a)
  instances:
    Predicate.pred :: (type) Sup
    bool :: Sup
    filter :: (type) Sup
    fset :: (type) Sup
    fun :: (type, complete_lattice) Sup
    real :: Sup
    set :: (type) Sup *)

subsection{*_,Z,Q,R,C: ab_group_add*}
  term "x::'a::ab_group_add"
  print_locale ab_group_add
  print_dependencies ab_group_add (*
class ab_group_add
  supersort: {cancel_comm_monoid_add,group_add}
  parameters:
  instances:
    complex :: ab_group_add
    int :: ab_group_add
    integer :: ab_group_add
    rat :: ab_group_add
    real :: ab_group_add *)

subsection{*N,Z,Q,R,C: ab_semigroup_add*}
  term "x::'a::ab_semigroup_add"
  print_locale ab_semigroup_add
  print_dependencies ab_semigroup_add (*
class ab_semigroup_add
  supersort: semigroup_add
  parameters:
  instances:
    complex :: ab_semigroup_add
    int :: ab_semigroup_add
    integer :: ab_semigroup_add
    multiset :: (type) ab_semigroup_add
    nat :: ab_semigroup_add
    natural :: ab_semigroup_add
    rat :: ab_semigroup_add
    real :: ab_semigroup_add *)

subsection{*N,Z,Q,R,C: ab_semigroup_mult*}
  term "x::'a::ab_semigroup_mult"
  print_locale ab_semigroup_mult
  print_dependencies ab_semigroup_mult (*
class ab_semigroup_mult
  supersort: semigroup_mult
  parameters:
  instances:
    complex :: ab_semigroup_mult
    int :: ab_semigroup_mult
    integer :: ab_semigroup_mult
    nat :: ab_semigroup_mult
    natural :: ab_semigroup_mult
    rat :: ab_semigroup_mult
    real :: ab_semigroup_mult *)

subsection{*_,Z,Q,R,_: abs*}
  term "x::'a::abs"
  print_locale abs
  print_dependencies abs (*
class abs
  supersort: type
  parameters:
    abs :: ('a \<Rightarrow> 'a)
  instances:
    int :: abs
    integer :: abs
    rat :: abs
    real :: abs *)

subsection{*_,Z,Q,R,_: abs_if*}
  term "x::'a::abs_if"
  print_locale abs_if
  print_dependencies abs_if (*
class abs_if
  supersort: {abs,minus,uminus,zero,ord}
  parameters:
  instances:
    int :: abs_if
    integer :: abs_if
    rat :: abs_if
    real :: abs_if *)

subsection{*_,_,Q,R,_: archimedean_field*}
  term "x::'a::archimedean_field"
  print_locale archimedean_field
  print_dependencies archimedean_field (*
class archimedean_field
  supersort: linordered_field
  parameters:
  instances:
    rat :: archimedean_field
    real :: archimedean_field *)

subsection{*_,_,_,R,C: banach*}
  term "x::'a::banach"
  print_locale banach
  print_dependencies banach (*
class banach
  supersort: {complete_space,real_normed_vector}
  parameters:
  instances:
    complex :: banach
    real :: banach *)

subsection{*_,_,_,_,_: boolean_algebra*}
  term "x::'a::boolean_algebra"
  print_locale boolean_algebra
  print_dependencies boolean_algebra (*
class boolean_algebra
  supersort: {minus,uminus,bounded_lattice,distrib_lattice}
  parameters:
  instances:
    Predicate.pred :: (type) boolean_algebra
    bool :: boolean_algebra
    fset :: (finite) boolean_algebra
    fun :: (type, boolean_algebra) boolean_algebra
    set :: (type) boolean_algebra *)

subsection{*N,_,_,_,_: bot*}
  term "x::'a::bot"
  print_locale bot
  print_dependencies bot (*
class bot
  supersort: type
  parameters:
    bot :: 'a
  instances:
    Predicate.pred :: (type) bot
    bool :: bot
    filter :: (type) bot
    fset :: (type) bot
    fun :: (type, bot) bot
    nat :: bot
    set :: (type) bot *)

subsection{*_,_,_,_,_: bounded_forall*}
  term "x::'a::bounded_forall"
  print_locale bounded_forall
  print_dependencies bounded_forall (*
class bounded_forall
  supersort: type
  parameters:
    bounded_forall :: (('a \<Rightarrow> bool) \<Rightarrow> (natural \<Rightarrow> bool)) *)

subsection{*_,_,_,_,_: bounded_lattice*}
  term "x::'a::bounded_lattice"
  print_locale bounded_lattice
  print_dependencies bounded_lattice (*
class bounded_lattice
  supersort: {bounded_lattice_bot,bounded_lattice_top}
  parameters:
  instances:
    Predicate.pred :: (type) bounded_lattice
    bool :: bounded_lattice
    filter :: (type) bounded_lattice
    fset :: (finite) bounded_lattice
    fun :: (type, bounded_lattice) bounded_lattice
    set :: (type) bounded_lattice *)

subsection{*_,_,_,_,_: bounded_lattice_bot*}
  term "x::'a::bounded_lattice_bot"
  print_locale bounded_lattice_bot
  print_dependencies bounded_lattice_bot (*
class bounded_lattice_bot
  supersort: {bounded_semilattice_sup_bot,lattice}
  parameters:
  instances:
    Predicate.pred :: (type) bounded_lattice_bot
    bool :: bounded_lattice_bot
    filter :: (type) bounded_lattice_bot
    fset :: (type) bounded_lattice_bot
    fun :: (type, bounded_lattice) bounded_lattice_bot
    set :: (type) bounded_lattice_bot *)

subsection{*_,_,_,_,_: bounded_lattice_top*}
  term "x::'a::bounded_lattice_top"
  print_locale bounded_lattice_top
  print_dependencies bounded_lattice_top (*
class bounded_lattice_top
  supersort: {bounded_semilattice_inf_top,lattice}
  parameters:
  instances:
    Predicate.pred :: (type) bounded_lattice_top
    bool :: bounded_lattice_top
    filter :: (type) bounded_lattice_top
    fset :: (finite) bounded_lattice_top
    fun :: (type, bounded_lattice) bounded_lattice_top
    set :: (type) bounded_lattice_top *)

subsection{*_,_,_,_,_: bounded_semilattice_inf_top*}
  term "x::'a::bounded_semilattice_inf_top"
  print_locale bounded_semilattice_inf_top
  print_dependencies bounded_semilattice_inf_top (*
class bounded_semilattice_inf_top
  supersort: {semilattice_inf,order_top}
  parameters:
  instances:
    Predicate.pred :: (type) bounded_semilattice_inf_top
    bool :: bounded_semilattice_inf_top
    filter :: (type) bounded_semilattice_inf_top
    fset :: (finite) bounded_semilattice_inf_top
    fun :: (type, bounded_lattice) bounded_semilattice_inf_top
    set :: (type) bounded_semilattice_inf_top *)

subsection{*_,_,_,_,_: bounded_semilattice_sup_bot*}
  term "x::'a::bounded_semilattice_sup_bot"
  print_locale bounded_semilattice_sup_bot
  print_dependencies bounded_semilattice_sup_bot (*
class bounded_semilattice_sup_bot
  supersort: {semilattice_sup,order_bot}
  parameters:
  instances:
    Predicate.pred :: (type) bounded_semilattice_sup_bot
    bool :: bounded_semilattice_sup_bot
    filter :: (type) bounded_semilattice_sup_bot
    fset :: (type) bounded_semilattice_sup_bot
    fun :: (type, bounded_lattice) bounded_semilattice_sup_bot
    set :: (type) bounded_semilattice_sup_bot *)

subsection{*N,Z,Q,R,C: cancel_ab_semigroup_add*}
  term "x::'a::cancel_ab_semigroup_add"
  print_locale cancel_ab_semigroup_add
  print_dependencies cancel_ab_semigroup_add (*
class cancel_ab_semigroup_add
  supersort: {ab_semigroup_add,cancel_semigroup_add}
  parameters:
  instances:
    complex :: cancel_ab_semigroup_add
    int :: cancel_ab_semigroup_add
    integer :: cancel_ab_semigroup_add
    multiset :: (type) cancel_ab_semigroup_add
    nat :: cancel_ab_semigroup_add
    natural :: cancel_ab_semigroup_add
    rat :: cancel_ab_semigroup_add
    real :: cancel_ab_semigroup_add *)

subsection{*N,Z,Q,R,C: cancel_comm_monoid_add*}
  term "x::'a::cancel_comm_monoid_add"
  print_locale cancel_comm_monoid_add
  print_dependencies cancel_comm_monoid_add (*
class cancel_comm_monoid_add
  supersort: {cancel_ab_semigroup_add,comm_monoid_add}
  parameters:
  instances:
    complex :: cancel_comm_monoid_add
    int :: cancel_comm_monoid_add
    integer :: cancel_comm_monoid_add
    multiset :: (type) cancel_comm_monoid_add
    nat :: cancel_comm_monoid_add
    natural :: cancel_comm_monoid_add
    rat :: cancel_comm_monoid_add
    real :: cancel_comm_monoid_add *)

subsection{*N,Z,Q,R,C: cancel_semigroup_add*}
  term "x::'a::cancel_semigroup_add"
  print_locale cancel_semigroup_add
  print_dependencies cancel_semigroup_add (*
class cancel_semigroup_add
  supersort: semigroup_add
  parameters:
  instances:
    complex :: cancel_semigroup_add
    int :: cancel_semigroup_add
    integer :: cancel_semigroup_add
    multiset :: (type) cancel_semigroup_add
    nat :: cancel_semigroup_add
    natural :: cancel_semigroup_add
    rat :: cancel_semigroup_add
    real :: cancel_semigroup_add *)

subsection{*_,_,_,_,_: ccpo*}
  term "x::'a::ccpo"
  print_locale ccpo
  print_dependencies ccpo (*
class ccpo
  supersort: {Sup,order}
  parameters:
  instances:
    Predicate.pred :: (type) ccpo
    bool :: ccpo
    filter :: (type) ccpo
    fset :: (finite) ccpo
    fun :: (type, complete_lattice) ccpo
    set :: (type) ccpo *)

subsection{*_,_,_,_,_: check_all*}
  term "x::'a::check_all"
  print_locale check_all
  print_dependencies check_all (*
class check_all
  supersort: {term_of,enum}
  parameters:
    check_all_class.check_all :: ((('a \<times> (unit \<Rightarrow> term)) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (bool \<times> term list) option)
    check_all_class.enum_  term_of :: ('a itself \<Rightarrow> (unit \<Rightarrow> term list))
  instances:
    Enum.finite_1 :: check_all
    Enum.finite_2 :: check_all
    Enum.finite_3 :: check_all
    Enum.finite_4 :: check_all
    bool :: check_all
    char :: check_all
    fun :: ({equal,check_all}, check_all) check_all
    nibble :: check_all
    option :: (check_all) check_all
    prod :: (check_all, check_all) check_all
    set :: (check_all) check_all
    sum :: (check_all, check_all) check_all
    unit :: check_all *)

subsection{*N,Z,Q,R,C: comm_monoid_add*}
  term "x::'a::comm_monoid_add"
  print_locale comm_monoid_add
  print_dependencies comm_monoid_add (*
class comm_monoid_add
  supersort: {ab_semigroup_add,monoid_add}
  parameters:
  instances:
    complex :: comm_monoid_add
    int :: comm_monoid_add
    integer :: comm_monoid_add
    multiset :: (type) comm_monoid_add
    nat :: comm_monoid_add
    natural :: comm_monoid_add
    rat :: comm_monoid_add
    real :: comm_monoid_add *)

subsection{*N,_,_,_,_: comm_monoid_diff*}
  term "x::'a::comm_monoid_diff"
  print_locale comm_monoid_diff
  print_dependencies comm_monoid_diff (*
class comm_monoid_diff
  supersort: {comm_monoid_add,minus}
  parameters:
  instances:
    multiset :: (type) comm_monoid_diff
    nat :: comm_monoid_diff
    natural :: comm_monoid_diff *)

subsection{*N,Z,Q,R,C: comm_monoid_mult*}
  term "x::'a::comm_monoid_mult"
  print_locale comm_monoid_mult
  print_dependencies comm_monoid_mult (*
class comm_monoid_mult
  supersort: {ab_semigroup_mult,monoid_mult}
  parameters:
  instances:
    complex :: comm_monoid_mult
    int :: comm_monoid_mult
    integer :: comm_monoid_mult
    nat :: comm_monoid_mult
    natural :: comm_monoid_mult
    rat :: comm_monoid_mult
    real :: comm_monoid_mult *)

subsection{*_,Z,Q,R,C: comm_ring*}
  term "x::'a::comm_ring"
  print_locale comm_ring
  print_dependencies comm_ring (*
class comm_ring
  supersort: {comm_semiring_0_cancel,ring}
  parameters:
  instances:
    complex :: comm_ring
    int :: comm_ring
    integer :: comm_ring
    rat :: comm_ring
    real :: comm_ring *)

subsection{*_,Z,Q,R,C: comm_ring_1*}
  term "x::'a::comm_ring_1"
  print_locale comm_ring_1
  print_dependencies comm_ring_1 (*
class comm_ring_1
  supersort: {comm_ring,comm_semiring_1_cancel,ring_1}
  parameters:
  instances:
    complex :: comm_ring_1
    int :: comm_ring_1
    integer :: comm_ring_1
    rat :: comm_ring_1
    real :: comm_ring_1 *)

subsection{*N,Z,Q,R,C: comm_semiring*}
  term "x::'a::comm_semiring"
  print_locale comm_semiring
  print_dependencies comm_semiring (*
class comm_semiring
  supersort: {ab_semigroup_mult,semiring}
  parameters:
  instances:
    complex :: comm_semiring
    int :: comm_semiring
    integer :: comm_semiring
    nat :: comm_semiring
    natural :: comm_semiring
    rat :: comm_semiring
    real :: comm_semiring *)

subsection{*N,Z,Q,R,C: comm_semiring_0*}
  term "x::'a::comm_semiring_0"
  print_locale comm_semiring_0
  print_dependencies comm_semiring_0 (*
class comm_semiring_0
  supersort: {comm_semiring,semiring_0}
  parameters:
  instances:
    complex :: comm_semiring_0
    int :: comm_semiring_0
    integer :: comm_semiring_0
    nat :: comm_semiring_0
    natural :: comm_semiring_0
    rat :: comm_semiring_0
    real :: comm_semiring_0 *)

subsection{*N,Z,Q,R,C: comm_semiring_0_cancel*}
  term "x::'a::comm_semiring_0_cancel"
  print_locale comm_semiring_0_cancel
  print_dependencies comm_semiring_0_cancel (*
class comm_semiring_0_cancel
  supersort: {comm_semiring_0,semiring_0_cancel}
  parameters:
  instances:
    complex :: comm_semiring_0_cancel
    int :: comm_semiring_0_cancel
    integer :: comm_semiring_0_cancel
    nat :: comm_semiring_0_cancel
    natural :: comm_semiring_0_cancel
    rat :: comm_semiring_0_cancel
    real :: comm_semiring_0_cancel *)

subsection{*N,Z,Q,R,C: comm_semiring_1*}
  term "x::'a::comm_semiring_1"
  print_locale comm_semiring_1
  print_dependencies comm_semiring_1 (*
class comm_semiring_1
  supersort: {comm_monoid_mult,comm_semiring_0,dvd,semiring_1}
  parameters:
  instances:
    complex :: comm_semiring_1
    int :: comm_semiring_1
    integer :: comm_semiring_1
    nat :: comm_semiring_1
    natural :: comm_semiring_1
    rat :: comm_semiring_1
    real :: comm_semiring_1 *)

subsection{*N,Z,Q,R,C: comm_semiring_1_cancel*}
  term "x::'a::comm_semiring_1_cancel"
  print_locale comm_semiring_1_cancel
  print_dependencies comm_semiring_1_cancel (*
class comm_semiring_1_cancel
  supersort: {comm_semiring_0_cancel,comm_semiring_1,semiring_1_cancel}
  parameters:
  instances:
    complex :: comm_semiring_1_cancel
    int :: comm_semiring_1_cancel
    integer :: comm_semiring_1_cancel
    nat :: comm_semiring_1_cancel
    natural :: comm_semiring_1_cancel
    rat :: comm_semiring_1_cancel
    real :: comm_semiring_1_cancel *)

subsection{*N,Z,Q,R,C: comm_semiring_1_cancel_crossproduct*}
  term "x::'a::comm_semiring_1_cancel_crossproduct"
  print_locale comm_semiring_1_cancel_crossproduct
  print_dependencies comm_semiring_1_cancel_crossproduct (*
class comm_semiring_1_cancel_crossproduct
  supersort: comm_semiring_1_cancel
  parameters:
  instances:
    complex :: comm_semiring_1_cancel_crossproduct
    int :: comm_semiring_1_cancel_crossproduct
    integer :: comm_semiring_1_cancel_crossproduct
    nat :: comm_semiring_1_cancel_crossproduct
    rat :: comm_semiring_1_cancel_crossproduct
    real :: comm_semiring_1_cancel_crossproduct *)

subsection{*_,_,_,_,_: complete_boolean_algebra*}
  term "x::'a::complete_boolean_algebra"
  print_locale complete_boolean_algebra
  print_dependencies complete_boolean_algebra (*
class complete_boolean_algebra
  supersort: {complete_distrib_lattice,boolean_algebra}
  parameters:
  instances:
    Predicate.pred :: (type) complete_boolean_algebra
    bool :: complete_boolean_algebra
    fset :: (finite) complete_boolean_algebra
    fun :: (type, complete_boolean_algebra) complete_boolean_algebra
    set :: (type) complete_boolean_algebra *)

subsection{*_,_,_,_,_: complete_distrib_lattice*}
  term "x::'a::complete_distrib_lattice"
  print_locale complete_distrib_lattice
  print_dependencies complete_distrib_lattice (*
class complete_distrib_lattice
  supersort: {complete_lattice,distrib_lattice}
  parameters:
  instances:
    Predicate.pred :: (type) complete_distrib_lattice
    bool :: complete_distrib_lattice
    fset :: (finite) complete_distrib_lattice
    fun :: (type, complete_distrib_lattice) complete_distrib_lattice
    set :: (type) complete_distrib_lattice *)

subsection{*_,_,_,_,_: complete_lattice*}
  term "x::'a::complete_lattice"
  print_locale complete_lattice
  print_dependencies complete_lattice (*
class complete_lattice
  supersort: {ccpo,conditionally_complete_lattice,bounded_lattice}
  parameters:
  instances:
    Predicate.pred :: (type) complete_lattice
    bool :: complete_lattice
    filter :: (type) complete_lattice
    fset :: (finite) complete_lattice
    fun :: (type, complete_lattice) complete_lattice
    set :: (type) complete_lattice *)

subsection{*_,_,_,_,_: complete_linorder*}
  term "x::'a::complete_linorder"
  print_locale complete_linorder
  print_dependencies complete_linorder (*
class complete_linorder
  supersort: {complete_distrib_lattice,linorder}
  parameters: *)

subsection{*_,_,_,R,C: complete_space*}
  term "x::'a::complete_space"
  print_locale complete_space
  print_dependencies complete_space (*
class complete_space
  supersort: metric_space
  parameters:
  instances:
    complex :: complete_space
    real :: complete_space *)

subsection{*_,_,_,R,_: conditionally_complete_lattice*}
  term "x::'a::conditionally_complete_lattice"
  print_locale conditionally_complete_lattice
  print_dependencies conditionally_complete_lattice (*
class conditionally_complete_lattice
  supersort: {Inf,Sup,lattice}
  parameters:
  instances:
    Predicate.pred :: (type) conditionally_complete_lattice
    bool :: conditionally_complete_lattice
    filter :: (type) conditionally_complete_lattice
    fset :: (type) conditionally_complete_lattice
    fun :: (type, complete_lattice) conditionally_complete_lattice
    real :: conditionally_complete_lattice
    set :: (type) conditionally_complete_lattice *)

subsection{*_,_,_,R,_: conditionally_complete_linorder*}
  term "x::'a::conditionally_complete_linorder"
  print_locale conditionally_complete_linorder
  print_dependencies conditionally_complete_linorder (*
class conditionally_complete_linorder
  supersort: {conditionally_complete_lattice,linorder}
  parameters:
  instances:
    real :: conditionally_complete_linorder *)

subsection{*N,Z,Q,_,_: countable*}
(*term "x::'a::countable"
  print_locale countable
  print_dependencies countable*) (*
class countable
  supersort: type
  parameters:
  instances:
    Enum.finite_1 :: countable
    Enum.finite_2 :: countable
    Enum.finite_3 :: countable
    Enum.finite_4 :: countable
    Enum.finite_5 :: countable
    String.literal :: countable
    bool :: countable
    char :: countable
    fset :: (finite) countable
    fun :: (finite, countable) countable
    int :: countable
    list :: (countable) countable
    nat :: countable
    nibble :: countable
    option :: (countable) countable
    prod :: (countable, countable) countable
    rat :: countable
    set :: (finite) countable
    sum :: (countable, countable) countable
    typerep :: countable
    unit :: countable *)

subsection{*_,_,_,_,_: default*}
  term "x::'a::default"
  print_locale default
  print_dependencies default (*
class default
  supersort: type
  parameters:
    default :: 'a
  instances:
    unit :: default *)

subsection{*_,_,Q,R,_: dense_linorder*}
  term "x::'a::dense_linorder"
  print_locale dense_linorder
  print_dependencies dense_linorder (*
class dense_linorder
  supersort: {dense_order,linorder}
  parameters:
  instances:
    rat :: dense_linorder
    real :: dense_linorder *)

subsection{*_,_,Q,R,_: dense_order*}
  term "x::'a::dense_order"
  print_locale dense_order
  print_dependencies dense_order (*
class dense_order
  supersort: order
  parameters:
  instances:
    rat :: dense_order
    real :: dense_order *)

subsection{*_,_,_,R,C: dist*}
  term "x::'a::dist"
  print_locale dist
  print_dependencies dist (*
class dist
  supersort: type
  parameters:
    dist :: ('a \<Rightarrow> ('a \<Rightarrow> real))
  instances:
    complex :: dist
    real :: dist *)

subsection{*_,_,_,R,C: dist_norm*}
  term "x::'a::dist_norm"
  print_locale dist_norm
  print_dependencies dist_norm (*
class dist_norm
  supersort: {minus,dist,norm}
  parameters:
  instances:
    complex :: dist_norm
    real :: dist_norm *)

subsection{*N,Z,Q,R,_: distrib_lattice*}
  term "x::'a::distrib_lattice"
  print_locale distrib_lattice
  print_dependencies distrib_lattice (*
class distrib_lattice
  supersort: lattice
  parameters:
  instances:
    Predicate.pred :: (type) distrib_lattice
    bool :: distrib_lattice
    fset :: (type) distrib_lattice
    fun :: (type, distrib_lattice) distrib_lattice
    int :: distrib_lattice
    nat :: distrib_lattice
    rat :: distrib_lattice
    real :: distrib_lattice
    set :: (type) distrib_lattice *)

subsection{*N,Z,_,_,_: div*}
  term "x::'a::Divides.div"
  print_locale div
  print_dependencies div (*
class div
  supersort: dvd
  parameters:
    div :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
    mod :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
  instances:
    int :: div
    integer :: div
    nat :: div
    natural :: div *)

subsection{*_,_,Q,R,C: division_ring*}
  term "x::'a::division_ring"
  print_locale division_ring
  print_dependencies division_ring (*
class division_ring
  supersort: {inverse,ring_1_no_zero_divisors}
  parameters:
  instances:
    complex :: division_ring
    rat :: division_ring
    real :: division_ring *)

subsection{*_,_,Q,R,C: division_ring_inverse_zero*}
  term "x::'a::division_ring_inverse_zero"
  print_locale division_ring_inverse_zero
  print_dependencies division_ring_inverse_zero (*
class division_ring_inverse_zero
  supersort: division_ring
  parameters:
  instances:
    complex :: division_ring_inverse_zero
    rat :: division_ring_inverse_zero
    real :: division_ring_inverse_zero *)

subsection{*N,Z,Q,R,C: dvd*}
  term "x::'a::Rings.dvd"
  print_locale dvd
  print_dependencies dvd (*
class dvd
  supersort: times
  parameters:
  instances:
    complex :: dvd
    int :: dvd
    integer :: dvd
    nat :: dvd
    natural :: dvd
    rat :: dvd
    real :: dvd *)

subsection{*_,_,_,_,_: enum*}
  term "x::'a::enum"
  print_locale enum
  print_dependencies enum (*
class enum
  supersort: finite
  parameters:
    enum_class.enum :: 'a list
    enum_class.enum_all :: (('a \<Rightarrow> bool) \<Rightarrow> bool)
    enum_class.enum_ex :: (('a \<Rightarrow> bool) \<Rightarrow> bool)
  instances:
    Enum.finite_1 :: enum
    Enum.finite_2 :: enum
    Enum.finite_3 :: enum
    Enum.finite_4 :: enum
    Enum.finite_5 :: enum
    bool :: enum
    char :: enum
    fun :: (enum, enum) enum
    nibble :: enum
    option :: (enum) enum
    prod :: (enum, enum) enum
    set :: (enum) enum
    sum :: (enum, enum) enum
    unit :: enum *)

subsection{*N,Z,Q,R,C: equal*}
  term "x::'a::equal"
  print_locale equal
  print_dependencies equal (*
class equal
  supersort: type
  parameters:
    equal_class.equal :: ('a \<Rightarrow> ('a \<Rightarrow> bool))
  instances:
    ??.Quickcheck_Narrowing.narrowing_cons :: (type) equal
    ??.Quickcheck_Narrowing.narrowing_  term :: equal
    ??.Quickcheck_Narrowing.narrowing_type :: equal
    ??.Quickcheck_Narrowing.property :: equal
    Enum.finite_1 :: equal
    Enum.finite_2 :: equal
    Enum.finite_3 :: equal
    Enum.finite_4 :: equal
    Enum.finite_5 :: equal
    Nitpick.fun_box :: (type, type) equal
    Nitpick.pair_box :: (type, type) equal
    Nitpick.word :: (type) equal
    Predicate.pred :: (type) equal
    Predicate.seq :: (type) equal
    Quickcheck_Exhaustive.three_valued :: (type) equal
    Quickcheck_Exhaustive.unknown :: (type) equal
    Quickcheck_Narrowing.cfun :: (type) equal
    Quickcheck_Narrowing.ffun :: (type, type) equal
    SMT.pattern :: equal
    String.literal :: equal
    bool :: equal
    char :: equal
    complex :: equal
    fset :: (equal) equal
    fun :: (enum, equal) equal
    int :: equal
    integer :: equal
    itself :: (type) equal
    lazy_sequence :: (type) equal
    list :: (type) equal
    multiset :: (equal) equal
    nat :: equal
    natural :: equal
    nibble :: equal
    num :: equal
    option :: (type) equal
    prod :: (type, type) equal
    rat :: equal
    real :: equal
    set :: (equal) equal
    sum :: (type, type) equal
    sumbool :: equal
      term :: equal
    tuple_isomorphism :: (type, type, type) equal
    typerep :: equal
    unit :: equal *)

subsection{*N,Z,_,_,_: even_odd*}
  term "x::'a::even_odd"
  print_locale even_odd
  print_dependencies even_odd (*
class even_odd
  supersort: type
  parameters:
    even :: ('a \<Rightarrow> bool)
  instances:
    int :: even_odd
    nat :: even_odd *)

subsection{*N,Z,Q,R,_: exhaustive*}
  term "x::'a::exhaustive"
  print_locale exhaustive
  print_dependencies exhaustive (*
class exhaustive
  supersort:   term_of
  parameters:
    exhaustive_class.exhaustive :: (('a \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (natural \<Rightarrow> (bool \<times> term list) option))
  instances:
    fun :: ({equal,exhaustive}, exhaustive) exhaustive
    int :: exhaustive
    integer :: exhaustive
    nat :: exhaustive
    natural :: exhaustive
    prod :: (exhaustive, exhaustive) exhaustive
    rat :: exhaustive
    real :: exhaustive
    set :: (exhaustive) exhaustive *)

subsection{*N,Z,_,_,_: fact*}
  term "x::'a::fact"
  print_locale fact
  print_dependencies fact (*
class fact
  supersort: type
  parameters:
    fact :: ('a \<Rightarrow> 'a)
  instances:
    int :: fact
    nat :: fact *)

subsection{*_,_,_,_,_: fast_exhaustive*}
  term "x::'a::fast_exhaustive"
  print_locale fast_exhaustive
  print_dependencies fast_exhaustive (*
class fast_exhaustive
  supersort:   term_of
  parameters:
    fast_exhaustive :: (('a \<Rightarrow> unit) \<Rightarrow> (natural \<Rightarrow> unit)) *)

subsection{*_,_,Q,R,C: field*}
  term "x::'a::field"
  print_locale field
  print_dependencies field (*
class field
  supersort: {division_ring,idom}
  parameters:
  instances:
    complex :: field
    rat :: field
    real :: field *)

subsection{*_,_,Q,R,C: field_char_0*}
  term "x::'a::field_char_0"
  print_locale field_char_0
  print_dependencies field_char_0 (*
class field_char_0
  supersort: {field,ring_char_0}
  parameters:
  instances:
    complex :: field_char_0
    rat :: field_char_0
    real :: field_char_0 *)

subsection{*_,_,Q,R,C: field_inverse_zero*}
  term "x::'a::field_inverse_zero"
  print_locale field_inverse_zero
  print_dependencies field_inverse_zero (*
class field_inverse_zero
  supersort: {division_ring_inverse_zero,field}
  parameters:
  instances:
    complex :: field_inverse_zero
    rat :: field_inverse_zero
    real :: field_inverse_zero *)

subsection{*_,_,_,_,_: finite*}
  term "x::'a::finite"
  print_locale finite
  print_dependencies finite (*
class finite
  supersort: countable
  parameters:
  instances:
    Enum.finite_1 :: finite
    Enum.finite_2 :: finite
    Enum.finite_3 :: finite
    Enum.finite_4 :: finite
    Enum.finite_5 :: finite
    bool :: finite
    char :: finite
    fset :: (finite) finite
    fun :: (finite, finite) finite
    nibble :: finite
    option :: (finite) finite
    prod :: (finite, finite) finite
    set :: (finite) finite
    sum :: (finite, finite) finite
    unit :: finite *)

subsection{*_,_,_,R,C: first_countable_topology*}
  term "x::'a::first_countable_topology"
  print_locale first_countable_topology
  print_dependencies first_countable_topology (*
class first_countable_topology
  supersort: topological_space
  parameters:
  instances:
    complex :: first_countable_topology
    real :: first_countable_topology *)

subsection{*_,_,Q,R,_: floor_ceiling*}
  term "x::'a::floor_ceiling"
  print_locale floor_ceiling
  print_dependencies floor_ceiling (*
class floor_ceiling
  supersort: archimedean_field
  parameters:
    floor :: ('a \<Rightarrow> int)
  instances:
    rat :: floor_ceiling
    real :: floor_ceiling *)

subsection{*N,Z,Q,R,C: full_exhaustive*}
  term "x::'a::full_exhaustive"
  print_locale full_exhaustive
  print_dependencies full_exhaustive (*
class full_exhaustive
  supersort:   term_of
  parameters:
    full_exhaustive_class.full_exhaustive :: ((('a \<times> (unit \<Rightarrow> term)) \<Rightarrow> (bool \<times> term list) option) \<Rightarrow> (natural \<Rightarrow> (bool \<times> term list) option))
  instances:
    ??.Quickcheck_Narrowing.narrowing_cons :: (full_exhaustive) full_exhaustive
    ??.Quickcheck_Narrowing.narrowing_  term :: full_exhaustive
    ??.Quickcheck_Narrowing.narrowing_type :: full_exhaustive
    Enum.finite_1 :: full_exhaustive
    Enum.finite_2 :: full_exhaustive
    Enum.finite_3 :: full_exhaustive
    Enum.finite_4 :: full_exhaustive
    Enum.finite_5 :: full_exhaustive
    Nitpick.fun_box :: ({equal,full_exhaustive}, full_exhaustive) full_exhaustive
    Nitpick.pair_box :: (full_exhaustive, full_exhaustive) full_exhaustive
    Nitpick.word :: (full_exhaustive) full_exhaustive
    Predicate.pred :: ({equal,full_exhaustive}) full_exhaustive
    Predicate.seq :: ({equal,full_exhaustive}) full_exhaustive
    Quickcheck_Exhaustive.three_valued :: (full_exhaustive) full_exhaustive
    Quickcheck_Exhaustive.unknown :: (full_exhaustive) full_exhaustive
    Quickcheck_Narrowing.cfun :: (full_exhaustive) full_exhaustive
    Quickcheck_Narrowing.ffun :: (full_exhaustive, full_exhaustive) full_exhaustive
    SMT.pattern :: full_exhaustive
    bool :: full_exhaustive
    char :: full_exhaustive
    complex :: full_exhaustive
    fun :: ({equal,full_exhaustive}, full_exhaustive) full_exhaustive
    int :: full_exhaustive
    integer :: full_exhaustive
    lazy_sequence :: (full_exhaustive) full_exhaustive
    list :: (full_exhaustive) full_exhaustive
    multiset :: (full_exhaustive) full_exhaustive
    nat :: full_exhaustive
    natural :: full_exhaustive
    nibble :: full_exhaustive
    num :: full_exhaustive
    option :: (full_exhaustive) full_exhaustive
    prod :: (full_exhaustive, full_exhaustive) full_exhaustive
    rat :: full_exhaustive
    real :: full_exhaustive
    set :: (full_exhaustive) full_exhaustive
    sum :: (full_exhaustive, full_exhaustive) full_exhaustive
    sumbool :: full_exhaustive
      term :: full_exhaustive
    tuple_isomorphism :: ({equal,full_exhaustive}, full_exhaustive, full_exhaustive) full_exhaustive
    unit :: full_exhaustive *)

subsection{*N,Z,_,_,_: gcd*}
  term "x::'a::gcd"
  print_locale gcd
  print_dependencies gcd (*
class gcd
  supersort: {one,zero,dvd}
  parameters:
    gcd :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
    lcm :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
  instances:
    int :: gcd
    nat :: gcd *)

subsection{*_,Z,Q,R,C: group_add*}
  term "x::'a::group_add"
  print_locale group_add
  print_dependencies group_add (*
class group_add
  supersort: {cancel_semigroup_add,minus,monoid_add,uminus}
  parameters:
  instances:
    complex :: group_add
    int :: group_add
    integer :: group_add
    rat :: group_add
    real :: group_add *)

subsection{*_,Z,Q,R,C: idom*}
  term "x::'a::idom"
  print_locale idom
  print_dependencies idom (*
class idom
  supersort: {comm_ring_1,ring_1_no_zero_divisors,comm_semiring_1_cancel_crossproduct}
  parameters:
  instances:
    complex :: idom
    int :: idom
    integer :: idom
    rat :: idom
    real :: idom *)

subsection{*N,Z,Q,R,_: inf*}
  term "x::'a::inf"
  print_locale inf
  print_dependencies inf (*
class inf
  supersort: type
  parameters:
    inf :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
  instances:
    Predicate.pred :: (type) inf
    bool :: inf
    filter :: (type) inf
    fset :: (type) inf
    fun :: (type, semilattice_inf) inf
    int :: inf
    multiset :: (type) inf
    nat :: inf
    rat :: inf
    real :: inf
    set :: (type) inf *)

subsection{*_,_,Q,R,C: inverse*}
  term "x::'a::inverse"
  print_locale inverse
  print_dependencies inverse (*
class inverse
  supersort: type
  parameters:
    inverse :: ('a \<Rightarrow> 'a)
    divide :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
  instances:
    complex :: inverse
    rat :: inverse
    real :: inverse *)

subsection{*_,_,_,_,_: is_testable*}
  term "x::'a::is_testable"
  print_locale is_testable
  print_dependencies is_testable (*
class is_testable
  supersort: type
  parameters:
  instances:
    bool :: is_testable
    fun :: ({  term_of,narrowing,partial_  term_of}, is_testable) is_testable *)

subsection{*N,Z,Q,R,_: lattice*}
  term "x::'a::lattice"
  print_locale lattice
  print_dependencies lattice (*
class lattice
  supersort: {semilattice_inf,semilattice_sup}
  parameters:
  instances:
    Predicate.pred :: (type) lattice
    bool :: lattice
    filter :: (type) lattice
    fset :: (type) lattice
    fun :: (type, lattice) lattice
    int :: lattice
    nat :: lattice
    rat :: lattice
    real :: lattice
    set :: (type) lattice *)

subsection{*_,_,_,R,_: linear_continuum*}
  term "x::'a::linear_continuum"
  print_locale linear_continuum
  print_dependencies linear_continuum (*
class linear_continuum
  supersort: {conditionally_complete_linorder,dense_linorder}
  parameters:
  instances:
    real :: linear_continuum *)

subsection{*_,_,_,R,_: linear_continuum_topology*}
  term "x::'a::linear_continuum_topology"
  print_locale linear_continuum_topology
  print_dependencies linear_continuum_topology (*
class linear_continuum_topology
  supersort: {linear_continuum,linorder_topology,perfect_space}
  parameters:
  instances:
    real :: linear_continuum_topology *)

subsection{*N,Z,Q,R,_: linorder*}
  term "x::'a::linorder"
  print_locale linorder
  print_dependencies linorder (*
class linorder
  supersort: order
  parameters:
  instances:
    Enum.finite_1 :: linorder
    Enum.finite_2 :: linorder
    Enum.finite_3 :: linorder
    bool :: linorder
    int :: linorder
    integer :: linorder
    nat :: linorder
    natural :: linorder
    num :: linorder
    rat :: linorder
    real :: linorder *)

subsection{*_,_,_,R,_: linorder_topology*}
  term "x::'a::linorder_topology"
  print_locale linorder_topology
  print_dependencies linorder_topology (*
class linorder_topology
  supersort: {linorder,order_topology,t2_space}
  parameters:
  instances:
    real :: linorder_topology *)

subsection{*_,Z,Q,R,_: linordered_ab_group_add*}
  term "x::'a::linordered_ab_group_add"
  print_locale linordered_ab_group_add
  print_dependencies linordered_ab_group_add (*
class linordered_ab_group_add
  supersort: {linordered_cancel_ab_semigroup_add,ordered_ab_group_add}
  parameters:
  instances:
    int :: linordered_ab_group_add
    integer :: linordered_ab_group_add
    rat :: linordered_ab_group_add
    real :: linordered_ab_group_add *)

subsection{*N,Z,Q,R,_: linordered_ab_semigroup_add*}
  term "x::'a::linordered_ab_semigroup_add"
  print_locale linordered_ab_semigroup_add
  print_dependencies linordered_ab_semigroup_add (*
class linordered_ab_semigroup_add
  supersort: {ordered_ab_semigroup_add,linorder}
  parameters:
  instances:
    int :: linordered_ab_semigroup_add
    integer :: linordered_ab_semigroup_add
    nat :: linordered_ab_semigroup_add
    natural :: linordered_ab_semigroup_add
    rat :: linordered_ab_semigroup_add
    real :: linordered_ab_semigroup_add *)

subsection{*N,Z,Q,R,_: linordered_cancel_ab_semigroup_add*}
  term "x::'a::linordered_cancel_ab_semigroup_add"
  print_locale linordered_cancel_ab_semigroup_add
  print_dependencies linordered_cancel_ab_semigroup_add (*
class linordered_cancel_ab_semigroup_add
  supersort: {linordered_ab_semigroup_add,ordered_ab_semigroup_add_imp_le}
  parameters:
  instances:
    int :: linordered_cancel_ab_semigroup_add
    integer :: linordered_cancel_ab_semigroup_add
    nat :: linordered_cancel_ab_semigroup_add
    natural :: linordered_cancel_ab_semigroup_add
    rat :: linordered_cancel_ab_semigroup_add
    real :: linordered_cancel_ab_semigroup_add *)

subsection{*N,Z,Q,R,_: linordered_comm_semiring_strict*}
  term "x::'a::linordered_comm_semiring_strict"
  print_locale linordered_comm_semiring_strict
  print_dependencies linordered_comm_semiring_strict (*
class linordered_comm_semiring_strict
  supersort: {linordered_semiring_strict,ordered_cancel_comm_semiring}
  parameters:
  instances:
    int :: linordered_comm_semiring_strict
    integer :: linordered_comm_semiring_strict
    nat :: linordered_comm_semiring_strict
    rat :: linordered_comm_semiring_strict
    real :: linordered_comm_semiring_strict *)

subsection{*_,_,Q,R,_: linordered_field*}
  term "x::'a::linordered_field"
  print_locale linordered_field
  print_dependencies linordered_field (*
class linordered_field
  supersort: {unbounded_dense_linorder,field_char_0,linordered_idom}
  parameters:
  instances:
    rat :: linordered_field
    real :: linordered_field *)

subsection{*_,_,Q,R,_: linordered_field_inverse_zero*}
  term "x::'a::linordered_field_inverse_zero"
  print_locale linordered_field_inverse_zero
  print_dependencies linordered_field_inverse_zero (*
class linordered_field_inverse_zero
  supersort: {field_inverse_zero,linordered_field}
  parameters:
  instances:
    rat :: linordered_field_inverse_zero
    real :: linordered_field_inverse_zero *)

subsection{*_,Z,Q,R,_: linordered_idom*}
  term "x::'a::linordered_idom"
  print_locale linordered_idom
  print_dependencies linordered_idom (*
class linordered_idom
  supersort: {sgn_if,ring_char_0,idom,linordered_ring_strict,linordered_semidom,linordered_semiring_1_strict,ordered_comm_ring,ordered_ring_abs}
  parameters:
  instances:
    int :: linordered_idom
    integer :: linordered_idom
    rat :: linordered_idom
    real :: linordered_idom *)

subsection{*_,Z,Q,R,_: linordered_ring*}
  term "x::'a::linordered_ring"
  print_locale linordered_ring
  print_dependencies linordered_ring (*
class linordered_ring
  supersort: {abs_if,linordered_ab_group_add,ordered_ab_group_add_abs,linordered_semiring,ordered_ring}
  parameters:
  instances:
    int :: linordered_ring
    integer :: linordered_ring
    rat :: linordered_ring
    real :: linordered_ring *)

subsection{*_,Z,Q,R,_: linordered_ring_strict*}
  term "x::'a::linordered_ring_strict"
  print_locale linordered_ring_strict
  print_dependencies linordered_ring_strict (*
class linordered_ring_strict
  supersort: {linordered_ring,linordered_semiring_strict,ring_no_zero_divisors}
  parameters:
  instances:
    int :: linordered_ring_strict
    integer :: linordered_ring_strict
    rat :: linordered_ring_strict
    real :: linordered_ring_strict *)

subsection{*N,Z,Q,R,_: linordered_semidom*}
  term "x::'a::linordered_semidom"
  print_locale linordered_semidom
  print_dependencies linordered_semidom (*
class linordered_semidom
  supersort: {semiring_char_0,comm_semiring_1_cancel,linordered_comm_semiring_strict}
  parameters:
  instances:
    int :: linordered_semidom
    integer :: linordered_semidom
    nat :: linordered_semidom
    rat :: linordered_semidom
    real :: linordered_semidom *)

subsection{*N,Z,Q,R,_: linordered_semiring*}
  term "x::'a::linordered_semiring"
  print_locale linordered_semiring
  print_dependencies linordered_semiring (*
class linordered_semiring
  supersort: {linordered_cancel_ab_semigroup_add,ordered_comm_monoid_add,ordered_cancel_semiring}
  parameters:
  instances:
    int :: linordered_semiring
    integer :: linordered_semiring
    nat :: linordered_semiring
    natural :: linordered_semiring
    rat :: linordered_semiring
    real :: linordered_semiring *)

subsection{*_,Z,Q,R,_: linordered_semiring_1*}
  term "x::'a::linordered_semiring_1"
  print_locale linordered_semiring_1
  print_dependencies linordered_semiring_1 (*
class linordered_semiring_1
  supersort: {linordered_semiring,semiring_1}
  parameters:
  instances:
    int :: linordered_semiring_1
    integer :: linordered_semiring_1
    rat :: linordered_semiring_1
    real :: linordered_semiring_1 *)

subsection{*_,Z,Q,R,_: linordered_semiring_1_strict*}
  term "x::'a::linordered_semiring_1_strict"
  print_locale linordered_semiring_1_strict
  print_dependencies linordered_semiring_1_strict (*
class linordered_semiring_1_strict
  supersort: {linordered_semiring_1,linordered_semiring_strict}
  parameters:
  instances:
    int :: linordered_semiring_1_strict
    integer :: linordered_semiring_1_strict
    rat :: linordered_semiring_1_strict
    real :: linordered_semiring_1_strict *)

subsection{*N,Z,Q,R,_: linordered_semiring_strict*}
  term "x::'a::linordered_semiring_strict"
  print_locale linordered_semiring_strict
  print_dependencies linordered_semiring_strict (*
class linordered_semiring_strict
  supersort: linordered_semiring
  parameters:
  instances:
    int :: linordered_semiring_strict
    integer :: linordered_semiring_strict
    nat :: linordered_semiring_strict
    rat :: linordered_semiring_strict
    real :: linordered_semiring_strict *)

subsection{*_,_,_,R,C: metric_space*}
  term "x::'a::metric_space"
  print_locale metric_space
  print_dependencies metric_space (*
class metric_space
  supersort: {open_dist,first_countable_topology,t2_space}
  parameters:
  instances:
    complex :: metric_space
    real :: metric_space *)

subsection{*N,Z,Q,R,C: minus*}
  term "x::'a::minus"
  print_locale minus
  print_dependencies minus (*
class minus
  supersort: type
  parameters:
    minus :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
  instances:
    Predicate.pred :: (type) minus
    bool :: minus
    complex :: minus
    fset :: (type) minus
    fun :: (type, minus) minus
    int :: minus
    integer :: minus
    multiset :: (type) minus
    nat :: minus
    natural :: minus
    rat :: minus
    real :: minus
    set :: (type) minus *)

subsection{*N,Z,Q,R,C: monoid_add*}
  term "x::'a::monoid_add"
  print_locale monoid_add
  print_dependencies monoid_add (*
class monoid_add
  supersort: {semigroup_add,zero}
  parameters:
  instances:
    complex :: monoid_add
    int :: monoid_add
    integer :: monoid_add
    multiset :: (type) monoid_add
    nat :: monoid_add
    natural :: monoid_add
    rat :: monoid_add
    real :: monoid_add *)

subsection{*N,Z,Q,R,C: monoid_mult*}
  term "x::'a::monoid_mult"
  print_locale monoid_mult
  print_dependencies monoid_mult (*
class monoid_mult
  supersort: {semigroup_mult,power}
  parameters:
  instances:
    complex :: monoid_mult
    int :: monoid_mult
    integer :: monoid_mult
    nat :: monoid_mult
    natural :: monoid_mult
    rat :: monoid_mult
    real :: monoid_mult *)

subsection{*N,Z,Q,R,C: mult_zero*}
  term "x::'a::mult_zero"
  print_locale mult_zero
  print_dependencies mult_zero (*
class mult_zero
  supersort: {times,zero}
  parameters:
  instances:
    complex :: mult_zero
    int :: mult_zero
    integer :: mult_zero
    nat :: mult_zero
    natural :: mult_zero
    rat :: mult_zero
    real :: mult_zero *)

subsection{*N,Z,Q,R,C: narrowing*}
  term "x::'a::narrowing"
  print_locale narrowing
  print_dependencies narrowing (*
class narrowing
  supersort: type
  parameters:
    narrowing :: (integer \<Rightarrow> 'a ??.Quickcheck_Narrowing.narrowing_cons)
  instances:
    ??.Quickcheck_Narrowing.narrowing_type :: narrowing
    Enum.finite_1 :: narrowing
    Enum.finite_2 :: narrowing
    Enum.finite_3 :: narrowing
    Enum.finite_4 :: narrowing
    Enum.finite_5 :: narrowing
    Nitpick.pair_box :: ({narrowing,typerep}, {narrowing,typerep}) narrowing
    Nitpick.word :: ({narrowing,typerep}) narrowing
    Quickcheck_Exhaustive.three_valued :: ({narrowing,typerep}) narrowing
    Quickcheck_Exhaustive.unknown :: ({narrowing,typerep}) narrowing
    Quickcheck_Narrowing.cfun :: ({narrowing,typerep}) narrowing
    Quickcheck_Narrowing.ffun :: ({narrowing,typerep}, {narrowing,typerep}) narrowing
    SMT.pattern :: narrowing
    bool :: narrowing
    char :: narrowing
    complex :: narrowing
    int :: narrowing
    integer :: narrowing
    lazy_sequence :: ({narrowing,typerep}) narrowing
    list :: ({narrowing,typerep}) narrowing
    nat :: narrowing
    natural :: narrowing
    nibble :: narrowing
    num :: narrowing
    option :: ({narrowing,typerep}) narrowing
    prod :: ({narrowing,typerep}, {narrowing,typerep}) narrowing
    rat :: narrowing
    real :: narrowing
    set :: (narrowing) narrowing
    sum :: ({narrowing,typerep}, {narrowing,typerep}) narrowing
    sumbool :: narrowing
      term :: narrowing
    unit :: narrowing *)

subsection{*_,Z,Q,R,C: neg_numeral*}
  term "x::'a::neg_numeral"
  print_locale neg_numeral
  print_dependencies neg_numeral (*
class neg_numeral
  supersort: {group_add,numeral}
  parameters:
  instances:
    complex :: neg_numeral
    int :: neg_numeral
    integer :: neg_numeral
    rat :: neg_numeral
    real :: neg_numeral *)

subsection{*_,Z,Q,R,_: no_bot*}
  term "x::'a::no_bot"
  print_locale no_bot
  print_dependencies no_bot (*
class no_bot
  supersort: order
  parameters:
  instances:
    int :: no_bot
    rat :: no_bot
    real :: no_bot *)

subsection{*N,Z,Q,R,_: no_top*}
  term "x::'a::no_top"
  print_locale no_top
  print_dependencies no_top (*
class no_top
  supersort: order
  parameters:
  instances:
    int :: no_top
    nat :: no_top
    rat :: no_top
    real :: no_top *)

subsection{*N,Z,Q,R,C: no_zero_divisors*}
  term "x::'a::no_zero_divisors"
  print_locale no_zero_divisors
  print_dependencies no_zero_divisors (*
class no_zero_divisors
  supersort: {times,zero}
  parameters:
  instances:
    complex :: no_zero_divisors
    int :: no_zero_divisors
    integer :: no_zero_divisors
    nat :: no_zero_divisors
    natural :: no_zero_divisors
    rat :: no_zero_divisors
    real :: no_zero_divisors *)

subsection{*_,_,_,R,C: norm*}
  term "x::'a::norm"
  print_locale norm
  print_dependencies norm (*
class norm
  supersort: type
  parameters:
    norm :: ('a \<Rightarrow> real)
  instances:
    complex :: norm
    real :: norm *)

subsection{*N,Z,Q,R,C: numeral*}
  term "x::'a::numeral"
  print_locale numeral
  print_dependencies numeral (*
class numeral
  supersort: {one,semigroup_add}
  parameters:
  instances:
    complex :: numeral
    int :: numeral
    integer :: numeral
    nat :: numeral
    natural :: numeral
    rat :: numeral
    real :: numeral *)

subsection{*N,Z,Q,R,C: one*}
  term "x::'a::one"
  print_locale one
  print_dependencies one (*
class one
  supersort: type
  parameters:
    one_class.one :: 'a
  instances:
    complex :: one
    int :: one
    integer :: one
    nat :: one
    natural :: one
    rat :: one
    real :: one *)

subsection{*_,_,_,R,C: open*}
  term "x::'a::open"
  print_locale Topological_Spaces.open
  print_dependencies Topological_Spaces.open (*
class open
  supersort: type
  parameters:
    open :: ('a set \<Rightarrow> bool)
  instances:
    complex :: open
    real :: open *)

subsection{*_,_,_,R,C: open_dist*}
  term "x::'a::open_dist"
  print_locale open_dist
  print_dependencies open_dist (*
class open_dist
  supersort: {dist,open}
  parameters:
  instances:
    complex :: open_dist
    real :: open_dist *)

subsection{*N,Z,Q,R,_: ord*}
  term "x::'a::ord"
  print_locale ord
  print_dependencies ord (*
class ord
  supersort: type
  parameters:
    less_eq :: ('a \<Rightarrow> ('a \<Rightarrow> bool))
    less :: ('a \<Rightarrow> ('a \<Rightarrow> bool))
  instances:
    Enum.finite_1 :: ord
    Enum.finite_2 :: ord
    Enum.finite_3 :: ord
    Predicate.pred :: (type) ord
    bool :: ord
    filter :: (type) ord
    fset :: (type) ord
    fun :: (type, ord) ord
    int :: ord
    integer :: ord
    multiset :: (type) ord
    nat :: ord
    natural :: ord
    num :: ord
    rat :: ord
    real :: ord
    set :: (type) ord *)

subsection{*N,Z,Q,R,_: order*}
  term "x::'a::order"
  print_locale order
  print_dependencies order (*
class order
  supersort: preorder
  parameters:
  instances:
    Enum.finite_1 :: order
    Enum.finite_2 :: order
    Enum.finite_3 :: order
    Predicate.pred :: (type) order
    bool :: order
    filter :: (type) order
    fset :: (type) order
    fun :: (type, order) order
    int :: order
    integer :: order
    multiset :: (type) order
    nat :: order
    natural :: order
    num :: order
    rat :: order
    real :: order
    set :: (type) order *)

subsection{*N,_,_,_,_: order_bot*}
  term "x::'a::order_bot"
  print_locale order_bot
  print_dependencies order_bot (*
class order_bot
  supersort: {bot,order}
  parameters:
  instances:
    Predicate.pred :: (type) order_bot
    bool :: order_bot
    filter :: (type) order_bot
    fset :: (type) order_bot
    fun :: (type, order_bot) order_bot
    nat :: order_bot
    set :: (type) order_bot *)

subsection{*_,_,_,_,_: order_top*}
  term "x::'a::order_top"
  print_locale order_top
  print_dependencies order_top (*
class order_top
  supersort: {order,top}
  parameters:
  instances:
    Predicate.pred :: (type) order_top
    bool :: order_top
    filter :: (type) order_top
    fset :: (finite) order_top
    fun :: (type, order_top) order_top
    set :: (type) order_top *)

subsection{*_,_,_,R,_: order_topology*}
  term "x::'a::order_topology"
  print_locale order_topology
  print_dependencies order_topology (*
class order_topology
  supersort: {order,topological_space}
  parameters:
  instances:
    real :: order_topology *)

subsection{*_,Z,Q,R,_: ordered_ab_group_add*}
  term "x::'a::ordered_ab_group_add"
  print_locale ordered_ab_group_add
  print_dependencies ordered_ab_group_add (*
class ordered_ab_group_add
  supersort: {ab_group_add,ordered_ab_semigroup_add_imp_le,ordered_comm_monoid_add}
  parameters:
  instances:
    int :: ordered_ab_group_add
    integer :: ordered_ab_group_add
    rat :: ordered_ab_group_add
    real :: ordered_ab_group_add *)

subsection{*_,Z,Q,R,_: ordered_ab_group_add_abs*}
  term "x::'a::ordered_ab_group_add_abs"
  print_locale ordered_ab_group_add_abs
  print_dependencies ordered_ab_group_add_abs (*
class ordered_ab_group_add_abs
  supersort: {abs,ordered_ab_group_add}
  parameters:
  instances:
    int :: ordered_ab_group_add_abs
    integer :: ordered_ab_group_add_abs
    rat :: ordered_ab_group_add_abs
    real :: ordered_ab_group_add_abs *)

subsection{*N,Z,Q,R,_: ordered_ab_semigroup_add*}
  term "x::'a::ordered_ab_semigroup_add"
  print_locale ordered_ab_semigroup_add
  print_dependencies ordered_ab_semigroup_add (*
class ordered_ab_semigroup_add
  supersort: {ab_semigroup_add,order}
  parameters:
  instances:
    int :: ordered_ab_semigroup_add
    integer :: ordered_ab_semigroup_add
    multiset :: (type) ordered_ab_semigroup_add
    nat :: ordered_ab_semigroup_add
    natural :: ordered_ab_semigroup_add
    rat :: ordered_ab_semigroup_add
    real :: ordered_ab_semigroup_add *)

subsection{*N,Z,Q,R,_: ordered_ab_semigroup_add_imp_le*}
  term "x::'a::ordered_ab_semigroup_add_imp_le"
  print_locale ordered_ab_semigroup_add_imp_le
  print_dependencies ordered_ab_semigroup_add_imp_le (*
class ordered_ab_semigroup_add_imp_le
  supersort: ordered_cancel_ab_semigroup_add
  parameters:
  instances:
    int :: ordered_ab_semigroup_add_imp_le
    integer :: ordered_ab_semigroup_add_imp_le
    multiset :: (type) ordered_ab_semigroup_add_imp_le
    nat :: ordered_ab_semigroup_add_imp_le
    natural :: ordered_ab_semigroup_add_imp_le
    rat :: ordered_ab_semigroup_add_imp_le
    real :: ordered_ab_semigroup_add_imp_le *)

subsection{*N,Z,Q,R,_: ordered_cancel_ab_semigroup_add*}
  term "x::'a::ordered_cancel_ab_semigroup_add"
  print_locale ordered_cancel_ab_semigroup_add
  print_dependencies ordered_cancel_ab_semigroup_add (*
class ordered_cancel_ab_semigroup_add
  supersort: {cancel_ab_semigroup_add,ordered_ab_semigroup_add}
  parameters:
  instances:
    int :: ordered_cancel_ab_semigroup_add
    integer :: ordered_cancel_ab_semigroup_add
    multiset :: (type) ordered_cancel_ab_semigroup_add
    nat :: ordered_cancel_ab_semigroup_add
    natural :: ordered_cancel_ab_semigroup_add
    rat :: ordered_cancel_ab_semigroup_add
    real :: ordered_cancel_ab_semigroup_add *)

subsection{*N,_,_,_,_: ordered_cancel_comm_monoid_diff*}
  term "x::'a::ordered_cancel_comm_monoid_diff"
  print_locale ordered_cancel_comm_monoid_diff
  print_dependencies ordered_cancel_comm_monoid_diff (*
class ordered_cancel_comm_monoid_diff
  supersort: {comm_monoid_diff,ordered_ab_semigroup_add_imp_le}
  parameters:
  instances:
    multiset :: (type) ordered_cancel_comm_monoid_diff
    nat :: ordered_cancel_comm_monoid_diff *)

subsection{*N,Z,Q,R,_: ordered_cancel_comm_semiring*}
  term "x::'a::ordered_cancel_comm_semiring"
  print_locale ordered_cancel_comm_semiring
  print_dependencies ordered_cancel_comm_semiring (*
class ordered_cancel_comm_semiring
  supersort: {comm_semiring_0_cancel,ordered_cancel_semiring,ordered_comm_semiring}
  parameters:
  instances:
    int :: ordered_cancel_comm_semiring
    integer :: ordered_cancel_comm_semiring
    nat :: ordered_cancel_comm_semiring
    rat :: ordered_cancel_comm_semiring
    real :: ordered_cancel_comm_semiring *)

subsection{*N,Z,Q,R,_: ordered_cancel_semiring*}
  term "x::'a::ordered_cancel_semiring"
  print_locale ordered_cancel_semiring
  print_dependencies ordered_cancel_semiring (*
class ordered_cancel_semiring
  supersort: {ordered_semiring,semiring_0_cancel}
  parameters:
  instances:
    int :: ordered_cancel_semiring
    integer :: ordered_cancel_semiring
    nat :: ordered_cancel_semiring
    natural :: ordered_cancel_semiring
    rat :: ordered_cancel_semiring
    real :: ordered_cancel_semiring *)

subsection{*N,Z,Q,R,_: ordered_comm_monoid_add*}
  term "x::'a::ordered_comm_monoid_add"
  print_locale ordered_comm_monoid_add
  print_dependencies ordered_comm_monoid_add (*
class ordered_comm_monoid_add
  supersort: {comm_monoid_add,ordered_cancel_ab_semigroup_add}
  parameters:
  instances:
    int :: ordered_comm_monoid_add
    integer :: ordered_comm_monoid_add
    nat :: ordered_comm_monoid_add
    natural :: ordered_comm_monoid_add
    rat :: ordered_comm_monoid_add
    real :: ordered_comm_monoid_add *)

subsection{*_,Z,Q,R,_: ordered_comm_ring*}
  term "x::'a::ordered_comm_ring"
  print_locale ordered_comm_ring
  print_dependencies ordered_comm_ring (*
class ordered_comm_ring
  supersort: {comm_ring,ordered_cancel_comm_semiring,ordered_ring}
  parameters:
  instances:
    int :: ordered_comm_ring
    integer :: ordered_comm_ring
    rat :: ordered_comm_ring
    real :: ordered_comm_ring *)

subsection{*N,Z,Q,R,_: ordered_comm_semiring*}
  term "x::'a::ordered_comm_semiring"
  print_locale ordered_comm_semiring
  print_dependencies ordered_comm_semiring (*
class ordered_comm_semiring
  supersort: {comm_semiring_0,ordered_semiring}
  parameters:
  instances:
    int :: ordered_comm_semiring
    integer :: ordered_comm_semiring
    nat :: ordered_comm_semiring
    rat :: ordered_comm_semiring
    real :: ordered_comm_semiring *)

subsection{*_,Z,Q,R,_: ordered_ring*}
  term "x::'a::ordered_ring"
  print_locale ordered_ring
  print_dependencies ordered_ring (*
class ordered_ring
  supersort: {ordered_ab_group_add,ordered_cancel_semiring,ring}
  parameters:
  instances:
    int :: ordered_ring
    integer :: ordered_ring
    rat :: ordered_ring
    real :: ordered_ring *)

subsection{*_,Z,Q,R,_: ordered_ring_abs*}
  term "x::'a::ordered_ring_abs"
  print_locale ordered_ring_abs
  print_dependencies ordered_ring_abs (*
class ordered_ring_abs
  supersort: {ordered_ab_group_add_abs,ordered_ring}
  parameters:
  instances:
    int :: ordered_ring_abs
    integer :: ordered_ring_abs
    rat :: ordered_ring_abs
    real :: ordered_ring_abs *)

subsection{*N,Z,Q,R,_: ordered_semiring*}
  term "x::'a::ordered_semiring"
  print_locale ordered_semiring
  print_dependencies ordered_semiring (*
class ordered_semiring
  supersort: {comm_monoid_add,ordered_ab_semigroup_add,semiring}
  parameters:
  instances:
    int :: ordered_semiring
    integer :: ordered_semiring
    nat :: ordered_semiring
    natural :: ordered_semiring
    rat :: ordered_semiring
    real :: ordered_semiring *)

subsection{*N,Z,Q,R,C: partial_  term_of*}
  term "x::'a::partial_term_of"
  print_locale partial_term_of
  print_dependencies partial_term_of (*
class partial_  term_of
  supersort: typerep
  parameters:
    partial_  term_of :: ('a itself \<Rightarrow> (??.Quickcheck_Narrowing.narrowing_  term \<Rightarrow>   term))
  instances:
    ??.Quickcheck_Narrowing.narrowing_cons :: (typerep) partial_  term_of
    ??.Quickcheck_Narrowing.narrowing_  term :: partial_  term_of
    ??.Quickcheck_Narrowing.narrowing_type :: partial_  term_of
    ??.Quickcheck_Narrowing.property :: partial_  term_of
    Enum.finite_1 :: partial_  term_of
    Enum.finite_2 :: partial_  term_of
    Enum.finite_3 :: partial_  term_of
    Enum.finite_4 :: partial_  term_of
    Enum.finite_5 :: partial_  term_of
    Nitpick.fun_box :: (typerep, typerep) partial_  term_of
    Nitpick.pair_box :: (typerep, typerep) partial_  term_of
    Nitpick.word :: (typerep) partial_  term_of
    Predicate.pred :: (typerep) partial_  term_of
    Predicate.seq :: (typerep) partial_  term_of
    Quickcheck_Exhaustive.three_valued :: (typerep) partial_  term_of
    Quickcheck_Exhaustive.unknown :: (typerep) partial_  term_of
    Quickcheck_Narrowing.cfun :: (typerep) partial_  term_of
    Quickcheck_Narrowing.ffun :: (typerep, typerep) partial_  term_of
    SMT.pattern :: partial_  term_of
    bool :: partial_  term_of
    char :: partial_  term_of
    complex :: partial_  term_of
    int :: partial_  term_of
    integer :: partial_  term_of
    itself :: (typerep) partial_  term_of
    lazy_sequence :: (typerep) partial_  term_of
    list :: (typerep) partial_  term_of
    multiset :: (typerep) partial_  term_of
    nat :: partial_  term_of
    natural :: partial_  term_of
    nibble :: partial_  term_of
    num :: partial_  term_of
    option :: (typerep) partial_  term_of
    prod :: (typerep, typerep) partial_  term_of
    rat :: partial_  term_of
    real :: partial_  term_of
    set :: (typerep) partial_  term_of
    sum :: (typerep, typerep) partial_  term_of
    sumbool :: partial_  term_of
      term :: partial_  term_of
    tuple_isomorphism :: (typerep, typerep, typerep) partial_  term_of
    typerep :: partial_  term_of
    unit :: partial_  term_of *)

subsection{*_,_,_,R,C: perfect_space*}
  term "x::'a::perfect_space"
  print_locale perfect_space
  print_dependencies perfect_space (*
class perfect_space
  supersort: topological_space
  parameters:
  instances:
    complex :: perfect_space
    real :: perfect_space *)

subsection{*N,Z,Q,R,C: plus*}
  term "x::'a::plus"
  print_locale plus
  print_dependencies plus (*
class plus
  supersort: type
  parameters:
    plus :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
  instances:
    complex :: plus
    int :: plus
    integer :: plus
    multiset :: (type) plus
    nat :: plus
    natural :: plus
    num :: plus
    rat :: plus
    real :: plus *)

subsection{*N,Z,Q,R,C: power*}
  term "x::'a::power"
  print_locale power
  print_dependencies power (*
class power
  supersort: {one,times}
  parameters:
  instances:
    complex :: power
    int :: power
    integer :: power
    nat :: power
    natural :: power
    rat :: power
    real :: power *)

subsection{*N,Z,Q,R,_: preorder*}
  term "x::'a::preorder"
  print_locale preorder
  print_dependencies preorder (*
class preorder
  supersort: ord
  parameters:
  instances:
    Enum.finite_1 :: preorder
    Enum.finite_2 :: preorder
    Enum.finite_3 :: preorder
    Predicate.pred :: (type) preorder
    bool :: preorder
    filter :: (type) preorder
    fset :: (type) preorder
    fun :: (type, preorder) preorder
    int :: preorder
    integer :: preorder
    multiset :: (type) preorder
    nat :: preorder
    natural :: preorder
    num :: preorder
    rat :: preorder
    real :: preorder
    set :: (type) preorder *)

subsection{*N,Z,Q,R,C: random*}
  term "x::'a::random"
  print_locale random
  print_dependencies random (*
class random
  supersort: typerep
  parameters:
    random_class.random :: (natural \<Rightarrow> ((natural \<times> natural) \<Rightarrow> (('a \<times> (unit \<Rightarrow> term)) \<times> (natural \<times> natural))))
  instances:
    ??.Quickcheck_Narrowing.narrowing_cons :: (random) random
    ??.Quickcheck_Narrowing.narrowing_  term :: random
    ??.Quickcheck_Narrowing.narrowing_type :: random
    ??.Quickcheck_Narrowing.property :: random
    Enum.finite_1 :: random
    Enum.finite_2 :: random
    Enum.finite_3 :: random
    Enum.finite_4 :: random
    Enum.finite_5 :: random
    Nitpick.fun_box :: ({  term_of,equal}, random) random
    Nitpick.pair_box :: (random, random) random
    Nitpick.word :: (random) random
    Predicate.pred :: ({  term_of,equal}) random
    Predicate.seq :: ({  term_of,equal,random}) random
    Quickcheck_Exhaustive.three_valued :: (random) random
    Quickcheck_Exhaustive.unknown :: (random) random
    Quickcheck_Narrowing.cfun :: (random) random
    Quickcheck_Narrowing.ffun :: (random, random) random
    SMT.pattern :: random
    String.literal :: random
    bool :: random
    char :: random
    complex :: random
    fun :: ({  term_of,equal}, random) random
    int :: random
    integer :: random
    itself :: (typerep) random
    lazy_sequence :: (random) random
    list :: (random) random
    multiset :: (random) random
    nat :: random
    natural :: random
    nibble :: random
    num :: random
    option :: (random) random
    prod :: (random, random) random
    rat :: random
    real :: random
    set :: (random) random
    sum :: (random, random) random
    sumbool :: random
      term :: random
    tuple_isomorphism :: ({  term_of,equal,random}, random, random) random
    typerep :: random
    unit :: random *)

subsection{*_,_,_,R,C: real_algebra*}
  term "x::'a::real_algebra"
  print_locale real_algebra
  print_dependencies real_algebra (*
class real_algebra
  supersort: {real_vector,ring}
  parameters:
  instances:
    complex :: real_algebra
    real :: real_algebra *)

subsection{*_,_,_,R,C: real_algebra_1*}
  term "x::'a::real_algebra_1"
  print_locale real_algebra_1
  print_dependencies real_algebra_1 (*
class real_algebra_1
  supersort: {ring_char_0,real_algebra}
  parameters:
  instances:
    complex :: real_algebra_1
    real :: real_algebra_1 *)

subsection{*_,_,_,R,C: real_div_algebra*}
  term "x::'a::real_div_algebra"
  print_locale real_div_algebra
  print_dependencies real_div_algebra (*
class real_div_algebra
  supersort: {division_ring,real_algebra_1}
  parameters:
  instances:
    complex :: real_div_algebra
    real :: real_div_algebra *)

subsection{*_,_,_,R,C: real_field*}
  term "x::'a::real_field"
  print_locale real_field
  print_dependencies real_field (*
class real_field
  supersort: {field_char_0,real_div_algebra}
  parameters:
  instances:
    complex :: real_field
    real :: real_field *)

subsection{*_,_,_,R,C: real_normed_algebra*}
  term "x::'a::real_normed_algebra"
  print_locale real_normed_algebra
  print_dependencies real_normed_algebra (*
class real_normed_algebra
  supersort: {real_algebra,real_normed_vector}
  parameters:
  instances:
    complex :: real_normed_algebra
    real :: real_normed_algebra *)

subsection{*_,_,_,R,C: real_normed_algebra_1*}
  term "x::'a::real_normed_algebra_1"
  print_locale real_normed_algebra_1
  print_dependencies real_normed_algebra_1 (*
class real_normed_algebra_1
  supersort: {real_algebra_1,real_normed_algebra,perfect_space}
  parameters:
  instances:
    complex :: real_normed_algebra_1
    real :: real_normed_algebra_1 *)

subsection{*_,_,_,R,C: real_normed_div_algebra*}
  term "x::'a::real_normed_div_algebra"
  print_locale real_normed_div_algebra
  print_dependencies real_normed_div_algebra (*
class real_normed_div_algebra
  supersort: {real_div_algebra,real_normed_algebra_1}
  parameters:
  instances:
    complex :: real_normed_div_algebra
    real :: real_normed_div_algebra *)

subsection{*_,_,_,R,C: real_normed_field*}
  term "x::'a::real_normed_field"
  print_locale real_normed_field
  print_dependencies real_normed_field (*
class real_normed_field
  supersort: {real_field,real_normed_div_algebra}
  parameters:
  instances:
    complex :: real_normed_field
    real :: real_normed_field *)

subsection{*_,_,_,R,C: real_normed_vector*}
  term "x::'a::real_normed_vector"
  print_locale real_normed_vector
  print_dependencies real_normed_vector (*
class real_normed_vector
  supersort: {dist_norm,metric_space,real_vector,sgn_div_norm}
  parameters:
  instances:
    complex :: real_normed_vector
    real :: real_normed_vector *)

subsection{*_,_,_,R,C: real_vector*}
  term "x::'a::real_vector"
  print_locale real_vector
  print_dependencies real_vector (*
class real_vector
  supersort: {ab_group_add,scaleR}
  parameters:
  instances:
    complex :: real_vector
    real :: real_vector *)

subsection{*_,Z,Q,R,C: ring*}
  term "x::'a::ring"
  print_locale ring
  print_dependencies ring (*
class ring
  supersort: {ab_group_add,semiring_0_cancel}
  parameters:
  instances:
    complex :: ring
    int :: ring
    integer :: ring
    rat :: ring
    real :: ring *)

subsection{*_,Z,Q,R,C: ring_1*}
  term "x::'a::ring_1"
  print_locale ring_1
  print_dependencies ring_1 (*
class ring_1
  supersort: {neg_numeral,ring,semiring_1_cancel}
  parameters:
  instances:
    complex :: ring_1
    int :: ring_1
    integer :: ring_1
    rat :: ring_1
    real :: ring_1 *)

subsection{*_,Z,Q,R,C: ring_1_no_zero_divisors*}
  term "x::'a::ring_1_no_zero_divisors"
  print_locale ring_1_no_zero_divisors
  print_dependencies ring_1_no_zero_divisors (*
class ring_1_no_zero_divisors
  supersort: {ring_1,ring_no_zero_divisors}
  parameters:
  instances:
    complex :: ring_1_no_zero_divisors
    int :: ring_1_no_zero_divisors
    integer :: ring_1_no_zero_divisors
    rat :: ring_1_no_zero_divisors
    real :: ring_1_no_zero_divisors *)

subsection{*_,Z,Q,R,C: ring_char_0*}
  term "x::'a::ring_char_0"
  print_locale ring_char_0
  print_dependencies ring_char_0 (*
class ring_char_0
  supersort: {semiring_char_0,ring_1}
  parameters:
  instances:
    complex :: ring_char_0
    int :: ring_char_0
    integer :: ring_char_0
    rat :: ring_char_0
    real :: ring_char_0 *)

subsection{*_,Z,_,_,_: ring_div*}
  term "x::'a::ring_div"
  print_locale ring_div
  print_dependencies ring_div (*
class ring_div
  supersort: {semiring_div,comm_ring_1,ring_1_no_zero_divisors}
  parameters:
  instances:
    int :: ring_div
    integer :: ring_div *)

subsection{*_,Z,Q,R,C: ring_no_zero_divisors*}
  term "x::'a::ring_no_zero_divisors"
  print_locale ring_no_zero_divisors
  print_dependencies ring_no_zero_divisors (*
class ring_no_zero_divisors
  supersort: {no_zero_divisors,ring}
  parameters:
  instances:
    complex :: ring_no_zero_divisors
    int :: ring_no_zero_divisors
    integer :: ring_no_zero_divisors
    rat :: ring_no_zero_divisors
    real :: ring_no_zero_divisors *)

subsection{*_,_,_,R,C: scaleR*}
  term "x::'a::scaleR"
  print_locale scaleR
  print_dependencies scaleR (*
class scaleR
  supersort: type
  parameters:
    scaleR :: (real \<Rightarrow> ('a \<Rightarrow> 'a))
  instances:
    complex :: scaleR
    real :: scaleR *)

subsection{*N,Z,Q,R,C: semigroup_add*}
  term "x::'a::semigroup_add"
  print_locale semigroup_add
  print_dependencies semigroup_add (*
class semigroup_add
  supersort: plus
  parameters:
  instances:
    complex :: semigroup_add
    int :: semigroup_add
    integer :: semigroup_add
    multiset :: (type) semigroup_add
    nat :: semigroup_add
    natural :: semigroup_add
    rat :: semigroup_add
    real :: semigroup_add *)

subsection{*N,Z,Q,R,C: semigroup_mult*}
  term "x::'a::semigroup_mult"
  print_locale semigroup_mult
  print_dependencies semigroup_mult (*
class semigroup_mult
  supersort: times
  parameters:
  instances:
    complex :: semigroup_mult
    int :: semigroup_mult
    integer :: semigroup_mult
    nat :: semigroup_mult
    natural :: semigroup_mult
    rat :: semigroup_mult
    real :: semigroup_mult *)

subsection{*N,Z,Q,R,_: semilattice_inf*}
  term "x::'a::semilattice_inf"
  print_locale semilattice_inf
  print_dependencies semilattice_inf (*
class semilattice_inf
  supersort: {inf,order}
  parameters:
  instances:
    Predicate.pred :: (type) semilattice_inf
    bool :: semilattice_inf
    filter :: (type) semilattice_inf
    fset :: (type) semilattice_inf
    fun :: (type, semilattice_inf) semilattice_inf
    int :: semilattice_inf
    multiset :: (type) semilattice_inf
    nat :: semilattice_inf
    rat :: semilattice_inf
    real :: semilattice_inf
    set :: (type) semilattice_inf *)

subsection{*N,Z,Q,R,_: semilattice_sup*}
  term "x::'a::semilattice_sup"
  print_locale semilattice_sup
  print_dependencies semilattice_sup (*
class semilattice_sup
  supersort: {sup,order}
  parameters:
  instances:
    Predicate.pred :: (type) semilattice_sup
    bool :: semilattice_sup
    filter :: (type) semilattice_sup
    fset :: (type) semilattice_sup
    fun :: (type, semilattice_sup) semilattice_sup
    int :: semilattice_sup
    multiset :: (type) semilattice_sup
    nat :: semilattice_sup
    rat :: semilattice_sup
    real :: semilattice_sup
    set :: (type) semilattice_sup *)

subsection{*N,Z,Q,R,C: semiring*}
  term "x::'a::semiring"
  print_locale semiring
  print_dependencies semiring (*
class semiring
  supersort: {ab_semigroup_add,semigroup_mult}
  parameters:
  instances:
    complex :: semiring
    int :: semiring
    integer :: semiring
    nat :: semiring
    natural :: semiring
    rat :: semiring
    real :: semiring *)

subsection{*N,Z,Q,R,C: semiring_0*}
  term "x::'a::semiring_0"
  print_locale semiring_0
  print_dependencies semiring_0 (*
class semiring_0
  supersort: {comm_monoid_add,mult_zero,semiring}
  parameters:
  instances:
    complex :: semiring_0
    int :: semiring_0
    integer :: semiring_0
    nat :: semiring_0
    natural :: semiring_0
    rat :: semiring_0
    real :: semiring_0 *)

subsection{*N,Z,Q,R,C: semiring_0_cancel*}
  term "x::'a::semiring_0_cancel"
  print_locale semiring_0_cancel
  print_dependencies semiring_0_cancel (*
class semiring_0_cancel
  supersort: {cancel_comm_monoid_add,semiring_0}
  parameters:
  instances:
    complex :: semiring_0_cancel
    int :: semiring_0_cancel
    integer :: semiring_0_cancel
    nat :: semiring_0_cancel
    natural :: semiring_0_cancel
    rat :: semiring_0_cancel
    real :: semiring_0_cancel *)

subsection{*N,Z,Q,R,C: semiring_1*}
  term "x::'a::semiring_1"
  print_locale semiring_1
  print_dependencies semiring_1 (*
class semiring_1
  supersort: {semiring_numeral,semiring_0,zero_neq_one}
  parameters:
  instances:
    complex :: semiring_1
    int :: semiring_1
    integer :: semiring_1
    nat :: semiring_1
    natural :: semiring_1
    rat :: semiring_1
    real :: semiring_1 *)

subsection{*N,Z,Q,R,C: semiring_1_cancel*}
  term "x::'a::semiring_1_cancel"
  print_locale semiring_1_cancel
  print_dependencies semiring_1_cancel (*
class semiring_1_cancel
  supersort: {semiring_0_cancel,semiring_1}
  parameters:
  instances:
    complex :: semiring_1_cancel
    int :: semiring_1_cancel
    integer :: semiring_1_cancel
    nat :: semiring_1_cancel
    natural :: semiring_1_cancel
    rat :: semiring_1_cancel
    real :: semiring_1_cancel *)

subsection{*N,Z,Q,R,C: semiring_char_0*}
  term "x::'a::semiring_char_0"
  print_locale semiring_char_0
  print_dependencies semiring_char_0 (*
class semiring_char_0
  supersort: semiring_1
  parameters:
  instances:
    complex :: semiring_char_0
    int :: semiring_char_0
    integer :: semiring_char_0
    nat :: semiring_char_0
    rat :: semiring_char_0
    real :: semiring_char_0 *)

subsection{*N,Z,_,_,_: semiring_div*}
  term "x::'a::semiring_div"
  print_locale semiring_div
  print_dependencies semiring_div (*
class semiring_div
  supersort: {div,comm_semiring_1_cancel,no_zero_divisors}
  parameters:
  instances:
    int :: semiring_div
    integer :: semiring_div
    nat :: semiring_div
    natural :: semiring_div *)

subsection{*N,Z,Q,R,C: semiring_numeral*}
  term "x::'a::semiring_numeral"
  print_locale semiring_numeral
  print_dependencies semiring_numeral (*
class semiring_numeral
  supersort: {monoid_mult,numeral,semiring}
  parameters:
  instances:
    complex :: semiring_numeral
    int :: semiring_numeral
    integer :: semiring_numeral
    nat :: semiring_numeral
    natural :: semiring_numeral
    rat :: semiring_numeral
    real :: semiring_numeral *) 

subsection{*N,Z,_,_,_: semiring_numeral_div*}
  term "x::'a::semiring_numeral_div"
  print_locale semiring_numeral_div
  print_dependencies semiring_numeral_div (*
class semiring_numeral_div
  supersort: {semiring_div,minus,linordered_semidom}
  parameters:
  instances:
    int :: semiring_numeral_div
    integer :: semiring_numeral_div
    nat :: semiring_numeral_div *)

subsection{*_,Z,Q,R,C: sgn*}
  term "x::'a::sgn"
  print_locale sgn
  print_dependencies sgn (*
class sgn
  supersort: type
  parameters:
    sgn :: ('a \<Rightarrow> 'a)
  instances:
    complex :: sgn
    int :: sgn
    integer :: sgn
    rat :: sgn
    real :: sgn *)

subsection{*_,_,_,R,C: sgn_div_norm*}
  term "x::'a::sgn_div_norm"
  print_locale sgn_div_norm
  print_dependencies sgn_div_norm (*
class sgn_div_norm
  supersort: {sgn,norm,scaleR}
  parameters:
  instances:
    complex :: sgn_div_norm
    real :: sgn_div_norm *)

subsection{*_,Z,Q,R,_: sgn_if*}
  term "x::'a::sgn_if"
  print_locale sgn_if
  print_dependencies sgn_if (*
class sgn_if
  supersort: {minus,one,sgn,uminus,zero,ord}
  parameters:
  instances:
    int :: sgn_if
    integer :: sgn_if
    rat :: sgn_if
    real :: sgn_if *)

subsection{*N,_,_,_,C: size*}
  term "x::'a::size"
  print_locale size
  print_dependencies size (*
class size
  supersort: type
  parameters:
    size :: ('a \<Rightarrow> nat)
  instances:
    ??.Quickcheck_Narrowing.narrowing_cons :: (type) size
    ??.Quickcheck_Narrowing.narrowing_  term :: size
    ??.Quickcheck_Narrowing.narrowing_type :: size
    Enum.finite_1 :: size
    Enum.finite_2 :: size
    Enum.finite_3 :: size
    Enum.finite_4 :: size
    Enum.finite_5 :: size
    Nitpick.fun_box :: (type, type) size
    Nitpick.pair_box :: (type, type) size
    Nitpick.word :: (type) size
    Predicate.pred :: (type) size
    Predicate.seq :: (type) size
    Quickcheck_Exhaustive.three_valued :: (type) size
    Quickcheck_Exhaustive.unknown :: (type) size
    Quickcheck_Narrowing.cfun :: (type) size
    Quickcheck_Narrowing.ffun :: (type, type) size
    SMT.pattern :: size
    String.literal :: size
    bool :: size
    char :: size
    complex :: size
    lazy_sequence :: (type) size
    list :: (type) size
    multiset :: (type) size
    nat :: size
    natural :: size
    nibble :: size
    num :: size
    option :: (type) size
    prod :: (type, type) size
    sum :: (type, type) size
    sumbool :: size
      term :: size
    tuple_isomorphism :: (type, type, type) size
    typerep :: size
    unit :: size *)

subsection{*_,Z,_,_,_: small_lazy*}
  term "x::'a::small_lazy"
  print_locale small_lazy
  print_dependencies small_lazy (*
class small_lazy
  supersort: type
  parameters:
    small_lazy :: (natural \<Rightarrow> 'a lazy_sequence)
  instances:
    int :: small_lazy
    list :: (small_lazy) small_lazy
    prod :: (small_lazy, small_lazy) small_lazy
    unit :: small_lazy *)

subsection{*N,Z,Q,R,_: sup*}
  term "x::'a::sup"
  print_locale sup
  print_dependencies sup (*
class sup
  supersort: type
  parameters:
    sup :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
  instances:
    Predicate.pred :: (type) sup
    bool :: sup
    filter :: (type) sup
    fset :: (type) sup
    fun :: (type, semilattice_sup) sup
    int :: sup
    multiset :: (type) sup
    nat :: sup
    rat :: sup
    real :: sup
    set :: (type) sup *)

subsection{*_,_,_,R,C: t0_space*}
  term "x::'a::t0_space"
  print_locale t0_space
  print_dependencies t0_space (*
class t0_space
  supersort: topological_space
  parameters:
  instances:
    complex :: t0_space
    real :: t0_space *)

subsection{*_,_,_,R,C: t1_space*}
  term "x::'a::t1_space"
  print_locale t1_space
  print_dependencies t1_space (*
class t1_space
  supersort: t0_space
  parameters:
  instances:
    complex :: t1_space
    real :: t1_space *)

subsection{*_,_,_,R,C: t2_space*}
  term "x::'a::t2_space"
  print_locale t2_space
  print_dependencies t2_space (*
class t2_space
  supersort: t1_space
  parameters:
  instances:
    complex :: t2_space
    real :: t2_space *)

subsection{*N,Z,Q,R,C: term_of*}
  term "x::'a::  term_of"
  print_locale   term_of
  print_dependencies   term_of (*
class   term_of
  supersort: typerep
  parameters:
      term_of_class.  term_of :: ('a \<Rightarrow>   term)
  instances:
    ??.Quickcheck_Narrowing.narrowing_cons :: (typerep)   term_of
    ??.Quickcheck_Narrowing.narrowing_  term ::   term_of
    ??.Quickcheck_Narrowing.narrowing_type ::   term_of
    ??.Quickcheck_Narrowing.property ::   term_of
    Enum.finite_1 ::   term_of
    Enum.finite_2 ::   term_of
    Enum.finite_3 ::   term_of
    Enum.finite_4 ::   term_of
    Enum.finite_5 ::   term_of
    Nitpick.fun_box :: (typerep, typerep)   term_of
    Nitpick.pair_box :: (typerep, typerep)   term_of
    Nitpick.word :: (typerep)   term_of
    Predicate.pred :: (typerep)   term_of
    Predicate.seq :: (typerep)   term_of
    Quickcheck_Exhaustive.three_valued :: (typerep)   term_of
    Quickcheck_Exhaustive.unknown :: (typerep)   term_of
    Quickcheck_Narrowing.cfun :: (typerep)   term_of
    Quickcheck_Narrowing.ffun :: (typerep, typerep)   term_of
    SMT.pattern ::   term_of
    String.literal ::   term_of
    bool ::   term_of
    char ::   term_of
    complex ::   term_of
    cset :: (typerep)   term_of
    fset :: (typerep)   term_of
    fun :: (typerep, typerep)   term_of
    int ::   term_of
    integer ::   term_of
    itself :: (typerep)   term_of
    lazy_sequence :: (typerep)   term_of
    list :: (typerep)   term_of
    multiset :: (typerep)   term_of
    nat ::   term_of
    natural ::   term_of
    nibble ::   term_of
    num ::   term_of
    option :: (typerep)   term_of
    prod :: (typerep, typerep)   term_of
    rat ::   term_of
    real ::   term_of
    set :: (typerep)   term_of
    sum :: (typerep, typerep)   term_of
    sumbool ::   term_of
      term ::   term_of
    tuple_isomorphism :: (typerep, typerep, typerep)   term_of
    typerep ::   term_of
    unit ::   term_of *)

subsection{*N,Z,Q,R,C: times*}
  term "x::'a::times"
  print_locale times
  print_dependencies times (*
class times
  supersort: type
  parameters:
    times :: ('a \<Rightarrow> ('a \<Rightarrow> 'a))
  instances:
    complex :: times
    int :: times
    integer :: times
    nat :: times
    natural :: times
    num :: times
    rat :: times
    real :: times *)

subsection{*_,_,_,_,_: top*}
  term "x::'a::top"
  print_locale top
  print_dependencies top (*
class top
  supersort: type
  parameters:
    top :: 'a
  instances:
    Predicate.pred :: (type) top
    bool :: top
    filter :: (type) top
    fset :: (finite) top
    fun :: (type, top) top
    set :: (type) top *)

subsection{*_,_,_,R,C: topological_space*}
  term "x::'a::topological_space"
  print_locale topological_space
  print_dependencies topological_space (*
class topological_space
  supersort: open
  parameters:
  instances:
    complex :: topological_space
    real :: topological_space *)

subsection{*N,Z,Q,R,C: type*}
  term "x::'a::type" (*  print_dependencies type*) (*
class type
  supersort: {}
  instances:
    ??.Quickcheck_Narrowing.narrowing_cons :: (type) type
    ??.Quickcheck_Narrowing.narrowing_  term :: type
    ??.Quickcheck_Narrowing.narrowing_type :: type
    ??.Quickcheck_Narrowing.property :: type
    Datatype.node :: (type, type) type
    Enum.finite_1 :: type
    Enum.finite_2 :: type
    Enum.finite_3 :: type
    Enum.finite_4 :: type
    Enum.finite_5 :: type
    Nitpick.bisim_iterator :: type
    Nitpick.fun_box :: (type, type) type
    Nitpick.pair_box :: (type, type) type
    Nitpick.signed_bit :: type
    Nitpick.unsigned_bit :: type
    Nitpick.word :: (type) type
    Predicate.pred :: (type) type
    Predicate.seq :: (type) type
    Quickcheck_Exhaustive.three_valued :: (type) type
    Quickcheck_Exhaustive.unknown :: (type) type
    Quickcheck_Narrowing.cfun :: (type) type
    Quickcheck_Narrowing.ffun :: (type, type) type
    SMT.pattern :: type
    String.literal :: type
    bool :: type
    char :: type
    complex :: type
    cset :: (type) type
    filter :: (type) type
    fset :: (type) type
    fun :: (type, type) type
    ind :: type
    int :: type
    integer :: type
    itself :: (type) type
    lazy_sequence :: (type) type
    list :: (type) type
    multiset :: (type) type
    nat :: type
    natural :: type
    nibble :: type
    num :: type
    option :: (type) type
    prod :: (type, type) type
    rD :: type
    rD.rD_IITN :: type
    rD_pre_rD_bdT :: type
    rat :: type
    real :: type
    set :: (type) type
    sum :: (type, type) type
    sumbool :: type
      term :: type
    tuple_isomorphism :: (type, type, type) type
    typerep :: type
    unit :: type *)

subsection{*N,Z,Q,R,C: typerep*}
  term "x::'a::typerep"
  print_locale typerep
  print_dependencies typerep (*
class typerep
  supersort: type
  parameters:
    typerep_class.typerep :: ('a itself \<Rightarrow> typerep)
  instances:
    ??.Quickcheck_Narrowing.narrowing_cons :: (typerep) typerep
    ??.Quickcheck_Narrowing.narrowing_  term :: typerep
    ??.Quickcheck_Narrowing.narrowing_type :: typerep
    ??.Quickcheck_Narrowing.property :: typerep
    Datatype.node :: (typerep, typerep) typerep
    Enum.finite_1 :: typerep
    Enum.finite_2 :: typerep
    Enum.finite_3 :: typerep
    Enum.finite_4 :: typerep
    Enum.finite_5 :: typerep
    Nitpick.fun_box :: (typerep, typerep) typerep
    Nitpick.pair_box :: (typerep, typerep) typerep
    Nitpick.word :: (typerep) typerep
    Predicate.pred :: (typerep) typerep
    Predicate.seq :: (typerep) typerep
    Quickcheck_Exhaustive.three_valued :: (typerep) typerep
    Quickcheck_Exhaustive.unknown :: (typerep) typerep
    Quickcheck_Narrowing.cfun :: (typerep) typerep
    Quickcheck_Narrowing.ffun :: (typerep, typerep) typerep
    SMT.pattern :: typerep
    String.literal :: typerep
    bool :: typerep
    char :: typerep
    complex :: typerep
    cset :: (typerep) typerep
    filter :: (typerep) typerep
    fset :: (typerep) typerep
    fun :: (typerep, typerep) typerep
    int :: typerep
    integer :: typerep
    itself :: (typerep) typerep
    lazy_sequence :: (typerep) typerep
    list :: (typerep) typerep
    multiset :: (typerep) typerep
    nat :: typerep
    natural :: typerep
    nibble :: typerep
    num :: typerep
    option :: (typerep) typerep
    prod :: (typerep, typerep) typerep
    rD :: typerep
    rD.rD_IITN :: typerep
    rD_pre_rD_bdT :: typerep
    rat :: typerep
    real :: typerep
    set :: (typerep) typerep
    sum :: (typerep, typerep) typerep
    sumbool :: typerep
      term :: typerep
    tuple_isomorphism :: (typerep, typerep, typerep) typerep
    typerep :: typerep
    unit :: typerep *)

subsection{*_,Z,Q,R,C: uminus*}
  term "x::'a::uminus"
  print_locale uminus
  print_dependencies uminus (*
class uminus
  supersort: type
  parameters:
    uminus :: ('a \<Rightarrow> 'a)
  instances:
    Predicate.pred :: (type) uminus
    bool :: uminus
    complex :: uminus
    fset :: (finite) uminus
    fun :: (type, uminus) uminus
    int :: uminus
    integer :: uminus
    rat :: uminus
    real :: uminus
    set :: (type) uminus *)

subsection{*_,_,Q,R,_: unbounded_dense_linorder*}
  term "x::'a::unbounded_dense_linorder"
  print_locale unbounded_dense_linorder
  print_dependencies unbounded_dense_linorder (*
class unbounded_dense_linorder
  supersort: {dense_linorder,no_bot,no_top}
  parameters:
  instances:
    rat :: unbounded_dense_linorder
    real :: unbounded_dense_linorder *)

subsection{*N,_,_,_,_: wellorder*}
  term "x::'a::wellorder"
  print_locale wellorder
  print_dependencies wellorder (*
class wellorder
  supersort: linorder
  parameters:
  instances:
    nat :: wellorder *)

subsection{*N,Z,Q,R,C: zero*}
  term "x::'a::zero"
  print_locale zero
  print_dependencies zero (*
class zero
  supersort: type
  parameters:
    zero_class.zero :: 'a
  instances:
    complex :: zero
    int :: zero
    integer :: zero
    multiset :: (type) zero
    nat :: zero
    natural :: zero
    rat :: zero
    real :: zero *)

subsection{*N,Z,Q,R,C: zero_neq_one*}
  term "x::'a::zero_neq_one"
  print_locale zero_neq_one
  print_dependencies zero_neq_one (*
class zero_neq_one:
  supersort: {one,zero}
  parameters:
  instances:
    complex :: zero_neq_one
    int :: zero_neq_one
    integer :: zero_neq_one
    nat :: zero_neq_one
    natural :: zero_neq_one
    rat :: zero_neq_one
    real :: zero_neq_one *)

 
end