84 | "bv_cvs CvsNil = []"

    84 | "bv_cvs CvsNil = []"

    85 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"

    85 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"

    86 

    86 

    87 (* generated theorems *)

    87 (* generated theorems *)

    88 

    88 

    89 thm core_haskell.perm_bn_alpha

    90 thm core_haskell.perm_bn_alpha

    90 thm core_haskell.perm_bn_simps

    91 thm core_haskell.perm_bn_simps

    91 thm core_haskell.bn_finite

    92 thm core_haskell.bn_finite

    92 

    93 

    93 thm core_haskell.distinct

    94 thm core_haskell.distinct