Loading theory "HOL-Library.AList" (required by "HOL-Quickcheck_Examples.Quickcheck_Examples" via "HOL-Library.DAList_Multiset" via "HOL-Library.DAList") Loading theory "HOL-Library.Confluence" (required by "HOL-Quickcheck_Examples.Quickcheck_Examples" via "HOL-Library.Dlist" via "HOL-Library.Confluent_Quotient") Loading theory "HOL-Library.Cancellation" (required by "HOL-Quickcheck_Examples.Quickcheck_Examples" via "HOL-Library.DAList_Multiset" via "HOL-Library.Multiset") Loading theory "HOL-Quickcheck_Examples.Completeness" Loading theory "HOL-Quickcheck_Examples.Quickcheck_Interfaces" Loading theory "HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples" ### Ignoring duplicate rewrite rule: ### \ \ ?x1 \ \ ### Ignoring duplicate rewrite rule: ### ?x1 \ \ \ \ ### theory "HOL-Library.Confluence" ### 0.140s elapsed time, 0.892s cpu time, 0.000s GC time Loading theory "HOL-Library.Confluent_Quotient" (required by "HOL-Quickcheck_Examples.Quickcheck_Examples" via "HOL-Library.Dlist") ### Ignoring duplicate rewrite rule: ### \ \ ?x1 \ \ ### Ignoring duplicate rewrite rule: ### ?x1 \ \ \ \ ### theory "HOL-Library.Confluent_Quotient" ### 0.137s elapsed time, 0.816s cpu time, 0.000s GC time Loading theory "HOL-Library.Dlist" (required by "HOL-Quickcheck_Examples.Quickcheck_Examples") ### theory "HOL-Quickcheck_Examples.Quickcheck_Lattice_Examples" ### 0.283s elapsed time, 1.744s cpu time, 0.000s GC time Loading theory "HOL-Quickcheck_Examples.Quickcheck_Nesting" (required by "HOL-Quickcheck_Examples.Quickcheck_Nesting_Example") ### theory "HOL-Quickcheck_Examples.Completeness" ### 0.455s elapsed time, 2.772s cpu time, 0.000s GC time *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available signature CANCEL = sig val proc: Proof.context -> cterm -> thm option end functor Cancel_Fun (Data: CANCEL_NUMERALS_DATA): CANCEL Found termination order: "(\p. size_list size (snd p)) <*mlex*> {}" val testers = [fn, fn, fn, fn]: (int -> bool) list val check_upto = fn: (int -> bool) -> int -> int -> bool ### theory "HOL-Quickcheck_Examples.Quickcheck_Interfaces" ### 0.519s elapsed time, 3.160s cpu time, 0.000s GC time signature CANCEL_DATA = sig val dest_coeff: term -> int * term val dest_sum: term -> term list val find_first_coeff: term -> term list -> int * term list val mk_coeff: int * term -> term val mk_sum: typ -> term list -> term val norm_ss1: simpset val norm_ss2: simpset val norm_tac: Proof.context -> tactic val numeral_simp_tac: Proof.context -> tactic val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option val simplify_meta_eq: Proof.context -> thm -> thm val trans_tac: Proof.context -> thm option -> tactic end structure Cancel_Data: CANCEL_DATA *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available signature CANCEL_SIMPROCS = sig val diff_cancel: Proof.context -> cterm -> thm option val eq_cancel: Proof.context -> cterm -> thm option val less_cancel: Proof.context -> cterm -> thm option val less_eq_cancel: Proof.context -> cterm -> thm option end structure Cancel_Simprocs: CANCEL_SIMPROCS ### theory "HOL-Library.Cancellation" ### 0.714s elapsed time, 4.308s cpu time, 0.000s GC time Loading theory "HOL-Library.Multiset" (required by "HOL-Quickcheck_Examples.Quickcheck_Examples" via "HOL-Library.DAList_Multiset") Proofs for inductive predicate(s) "double" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... val it = (): unit ### theory "HOL-Quickcheck_Examples.Quickcheck_Nesting" ### 0.685s elapsed time, 3.996s cpu time, 0.476s GC time Loading theory "HOL-Quickcheck_Examples.Quickcheck_Nesting_Example" ### theory "HOL-Library.Dlist" ### 0.793s elapsed time, 4.652s cpu time, 0.476s GC time *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available val it = [false, true, true, true]: bool list val it = [false, false, true, true]: bool list val it = [false, false, true, true]: bool list *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available val it = [false, false, false, true]: bool list Found termination order: "(\p. size_list size (snd (snd p))) <*mlex*> {}" ### Rule already declared as introduction (intro) ### (\x. ?f x = ?g x) \ ?f = ?g *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available ### Partially applied constant "Multiset.inf_subset_mset" on left hand side of equation, in theorem: ### semilattice_inf.Inf_fin (\#) (set (?x # ?xs)) \ fold (\#) ?xs ?x Found termination order: "(\p. size_list size (snd (snd (snd p)))) <*mlex*> {}" ### Partially applied constant "Multiset.sup_subset_mset" on left hand side of equation, in theorem: ### semilattice_sup.Sup_fin (\#) (set (?x # ?xs)) \ fold (\#) ?xs ?x ### theory "HOL-Library.AList" ### 1.625s elapsed time, 9.692s cpu time, 0.476s GC time Loading theory "HOL-Library.DAList" (required by "HOL-Quickcheck_Examples.Quickcheck_Examples" via "HOL-Library.DAList_Multiset") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available ### theory "HOL-Quickcheck_Examples.Quickcheck_Nesting_Example" ### 0.736s elapsed time, 4.444s cpu time, 0.000s GC time *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available Found termination order: "(\p. size (fst p)) <*mlex*> {}" signature MULTISET_SIMPROCS = sig val subset_cancel_msets: Proof.context -> cterm -> thm option val subseteq_cancel_msets: Proof.context -> cterm -> thm option end structure Multiset_Simprocs: MULTISET_SIMPROCS ### Additional type variable(s) in specification of "random_aux_alist_rel": 'a, 'b ### Additional type variable(s) in specification of "random_aux_alist_dom": 'a, 'b Found termination order: "(\p. nat_of_natural (fst p)) <*mlex*> {}" Found termination order: "(\p. nat_of_natural (snd p)) <*mlex*> {}" Found termination order: "(\p. nat_of_natural (snd p)) <*mlex*> {}" ### theory "HOL-Library.DAList" ### 1.490s elapsed time, 8.764s cpu time, 0.840s GC time *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available ### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__" ### Introduced fixed type variable(s): 'h in "A__" Proofs for inductive predicate(s) "pw_leq" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... Found termination order: "(\p. length (fst p)) <*mlex*> {}" Proofs for inductive predicate(s) "pred_mset" Proving monotonicity ... Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Introduced fixed type variable(s): 'd, 'e, 'f in "f__" or "g__" ### Introduced fixed type variable(s): 'd, 'e in "X__" or "f__" or "g__" ### Introduced fixed type variable(s): 'd, 'e in "f__" ### Introduced fixed type variable(s): 'd in "X__" ### Introduced fixed type variable(s): 'd, 'e, 'f in "R__" or "S__" Proofs for inductive predicate(s) "rel_mset'" Proving monotonicity ... ### Introduced fixed type variable(s): 'd, 'e in "R__" Proving the introduction rules ... Proving the elimination rules ... Proving the induction rule ... Proving the simplification rules ... ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Ignoring duplicate rewrite rule: ### mset (map ?f1 ?xs1) \ image_mset ?f1 (mset ?xs1) ### Introduced fixed type variable(s): 'd in "z__" ### Introduced fixed type variable(s): 'd in "P__" ### theory "HOL-Library.Multiset" ### 4.933s elapsed time, 28.984s cpu time, 2.300s GC time Loading theory "HOL-Library.DAList_Multiset" (required by "HOL-Quickcheck_Examples.Quickcheck_Examples") Found termination order: "(\p. size_list (\p. size (snd p)) (snd (snd p))) <*mlex*> {}" ### theory "HOL-Library.DAList_Multiset" ### 0.671s elapsed time, 4.024s cpu time, 0.000s GC time Loading theory "HOL-Quickcheck_Examples.Quickcheck_Examples" ### Introduced fixed type variable(s): 'b in "a__" or "x__" *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available ### theory "HOL-Quickcheck_Examples.Quickcheck_Examples" ### 4.509s elapsed time, 8.232s cpu time, 0.632s GC time *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 597 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 592 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 587 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 582 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 577 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 572 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 567 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 557 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 553 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 548 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 538 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 537 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 536 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 532 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 531 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 530 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 525 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 524 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 523 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 516 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 511 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 506 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 497 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 498 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 490 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 483 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 482 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 468 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 457 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 446 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 445 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 435 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 434 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 422 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 423 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 417 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 416 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 409 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 405 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 401 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 397 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 391 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 390 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 385 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 386 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 380 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 379 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 374 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 375 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 368 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 369 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 363 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 362 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 351 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 350 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 345 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 344 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 339 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 338 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 331 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 330 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 322 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 317 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 312 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 301 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 296 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 288 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 283 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 275 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 274 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 269 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 270 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 265 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 264 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 254 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 253 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 245 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 244 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 239 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 238 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 233 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 232 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 227 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 226 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 221 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 220 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 215 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 214 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 209 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 208 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 203 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 202 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 197 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 196 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 191 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 190 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 185 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 184 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 178 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 177 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 165 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 164 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 148 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 149 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 143 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 142 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 119 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 118 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 113 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 112 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 103 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 102 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 97 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 96 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 92 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 91 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 77 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 76 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 72 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 71 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 60 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 59 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 58 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 57 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 56 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 55 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 51 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 50 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 46 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 45 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 41 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 40 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 39 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 35 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 34 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 29 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 30 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 8 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Nesting_Example.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 131 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 126 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 121 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 116 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 111 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 106 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 101 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 96 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 76 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 56 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 29 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 91 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 86 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 81 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 71 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 66 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 61 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 49 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 44 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 39 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy") *** exception Fail raised (line 683 of "statistics.cpp"): No statistics available *** At command "quickcheck" (line 34 of "~~/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy")