Failed to load theory "Actuarial_Mathematics.Interest" (unresolved "Actuarial_Mathematics.Preliminaries_AC")
Failed to load theory "Actuarial_Mathematics.Survival_Model" (unresolved "Actuarial_Mathematics.Preliminaries_AC")
Failed to load theory "Actuarial_Mathematics.Life_Table" (unresolved "Actuarial_Mathematics.Survival_Model")
Failed to load theory "Actuarial_Mathematics.Examples" (unresolved "Actuarial_Mathematics.Life_Table")
Failed to finish proof (line 800 of "~~/dirs/AFP/thys/Actuarial_Mathematics/Preliminaries_AC.thy"):
goal (1 subgoal):
1. (⋀x. a < x ∧ x < b ∧ x ∉ S ⟹
(F has_vector_derivative deriv F x) (at x)) ⟹
countable
S
At command "by" (line 799 of "~~/dirs/AFP/thys/Actuarial_Mathematics/Preliminaries_AC.thy")
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Zeta_Function.Zeta_Library" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal" (unresolved "Zeta_Function.Zeta_Library")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal")
Failed to load theory "Negative_Association.Negative_Association_Permutation_Distributions" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm")
Failed to load theory "CVM_Distinct_Elements.CVM_New_Unbiased_Algorithm" (unresolved "Negative_Association.Negative_Association_Permutation_Distributions")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?s; ?a ≤ ?b; ?g ` {?a..?b} ⊆ {?c..?d};
continuous_on {?c..?d} ?f; continuous_on {?a..?b} ?g;
⋀x. x ∈ {?a..?b} - ?s ⟹
(?g has_real_derivative ?g' x) (at x within {?a..?b})⟧
⟹ ((λx. ?g' x *⇩R ?f (?g x)) has_integral
integral {?g ?a..?g ?b} ?f - integral {?g ?b..?g ?a} ?f)
{?a..?b}
finite {- 1, 1}
- 1 ≤ 1
arccos ` {- 1..1} ⊆ {0..pi}
continuous_on {0..pi} (λt. - cos (real m * t) * cos (real n * t))
continuous_on {- 1..1} arccos
?x ∈ {- 1..1} - {- 1, 1} ⟹
(arccos has_real_derivative - inverse (sqrt (1 - ?x⇧2)))
(at ?x
within {- 1..1})
At command "from" (line 2328 of "~~/dirs/AFP/thys/Chebyshev_Polynomials/Chebyshev_Polynomials.thy")
Timeout
Solver verit: Solver terminated abnormally with error code 127 At command "by" (line 834 of "~~/dirs/AFP/thys/Difference_Bound_Matrices/DBM_Constraint_Systems.thy")
Timeout
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Euler_MacLaurin.Euler_MacLaurin_Landau" (unresolved "Euler_MacLaurin.Euler_MacLaurin")
Failed to load theory "Dirichlet_Series.Arithmetic_Summatory_Asymptotics" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis", "Euler_MacLaurin.Euler_MacLaurin_Landau")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a<..<?b} - ?S ⟹ (?f has_vector_derivative ?f' x) (at x);
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
Y
At command "by" (line 739 of "~~/dirs/AFP/thys/Euler_MacLaurin/Euler_MacLaurin.thy")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Zeta_Function.Zeta_Library" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal" (unresolved "Zeta_Function.Zeta_Library")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal")
Failed to load theory "Finite_Fields.Find_Irreducible_Poly" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm")
Failed to load theory "Universal_Hash_Families.Pseudorandom_Objects_Hash_Families" (unresolved "Finite_Fields.Find_Irreducible_Poly")
Failed to load theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm" (unresolved "Universal_Hash_Families.Pseudorandom_Objects_Hash_Families")
Failed to load theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff" (unresolved "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Inner_Algorithm")
Failed to load theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level" (unresolved "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff")
Failed to load theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy" (unresolved "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy_Without_Cutoff", "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Cutoff_Level")
Failed to load theory "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Outer_Algorithm" (unresolved "Distributed_Distinct_Elements.Distributed_Distinct_Elements_Accuracy")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
Failed to load theory "Euler_MacLaurin.Euler_MacLaurin_Landau" (unresolved "Euler_MacLaurin.Euler_MacLaurin")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a<..<?b} - ?S ⟹ (?f has_vector_derivative ?f' x) (at x);
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
Y
At command "by" (line 739 of "~~/dirs/AFP/thys/Euler_MacLaurin/Euler_MacLaurin.thy")
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Zeta_Function.Zeta_Library" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal" (unresolved "Zeta_Function.Zeta_Library")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal")
Failed to load theory "Executable_Randomized_Algorithms.Basic_Randomized_Algorithms" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm")
Failed to load theory "Executable_Randomized_Algorithms.Tracking_Randomized_Algorithm" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm")
Failed to load theory "Executable_Randomized_Algorithms.Tracking_SPMF" (unresolved "Executable_Randomized_Algorithms.Tracking_Randomized_Algorithm")
Failed to load theory "Executable_Randomized_Algorithms.Dice_Roll" (unresolved "Executable_Randomized_Algorithms.Tracking_SPMF")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Zeta_Function.Zeta_Library" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal" (unresolved "Zeta_Function.Zeta_Library")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal")
Failed to load theory "Finite_Fields.Find_Irreducible_Poly" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Zeta_Function.Zeta_Library" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal" (unresolved "Zeta_Function.Zeta_Library")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal")
Failed to load theory "Finite_Fields.Find_Irreducible_Poly" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm")
Failed to load theory "Universal_Hash_Families.Pseudorandom_Objects_Hash_Families" (unresolved "Finite_Fields.Find_Irreducible_Poly")
Failed to load theory "Frequency_Moments.Tutorial_Pseudorandom_Objects" (unresolved "Universal_Hash_Families.Pseudorandom_Objects_Hash_Families")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
Failed to load theory "Green.Paths" (unresolved "Green.Integrals")
Failed to load theory "Green.Green" (unresolved "Green.Integrals", "Green.Paths")
Failed to load theory "Green.SymmetricR2Shapes" (unresolved "Green.Green")
Failed to load theory "Green.CircExample" (unresolved "Green.Green", "Green.SymmetricR2Shapes")
Failed to load theory "Green.DiamExample" (unresolved "Green.Green", "Green.SymmetricR2Shapes")
Failed to apply initial proof method (line 722 of "~~/dirs/AFP/thys/Green/Integrals.thy"):
using this:
finite S
a ≤ b
?x ∈ {a<..<b} - S ⟹
(f has_vector_derivative f' ?x) (at ?x within {a..b} - S)
continuous_on {a..b} f
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a<..<?b} - ?S ⟹ (?f has_vector_derivative ?f' x) (at x);
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
⟦?x ∈ box ?a ?b; ?x ∉ ?S; finite ?S⟧
⟹ at ?x within cbox ?a ?b - ?S = at ?x
goal (1 subgoal):
1. (f' has_integral f b - f a)
{a..b}
At command "by" (line 722 of "~~/dirs/AFP/thys/Green/Integrals.thy")
Timeout
Timeout
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Zeta_Function.Zeta_Library" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal" (unresolved "Zeta_Function.Zeta_Library")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal")
Failed to load theory "Negative_Association.Negative_Association_Permutation_Distributions" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm")
Failed to load theory "Negative_Association.Negative_Association_Bloom_Filters" (unresolved "Negative_Association.Negative_Association_Permutation_Distributions")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
Timeout
Timeout
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Zeta_Function.Zeta_Library" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis")
Failed to load theory "Zeta_Function.Zeta_Function" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis", "Euler_MacLaurin.Euler_MacLaurin", "Zeta_Function.Zeta_Library")
Failed to load theory "Dirichlet_L.Dirichlet_L_Functions" (unresolved "Zeta_Function.Zeta_Function")
Failed to load theory "Dirichlet_L.Dirichlet_Theorem" (unresolved "Dirichlet_L.Dirichlet_L_Functions")
Failed to load theory "Three_Squares.Three_Squares" (unresolved "Dirichlet_L.Dirichlet_Theorem")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a<..<?b} - ?S ⟹ (?f has_vector_derivative ?f' x) (at x);
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
Y
At command "by" (line 739 of "~~/dirs/AFP/thys/Euler_MacLaurin/Euler_MacLaurin.thy")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
Timeout
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Zeta_Function.Zeta_Library" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis")
Failed to load theory "Zeta_Function.Zeta_Function" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis", "Euler_MacLaurin.Euler_MacLaurin", "Zeta_Function.Zeta_Library")
Failed to load theory "Prime_Number_Theorem.Prime_Number_Theorem_Library" (unresolved "Zeta_Function.Zeta_Function")
Failed to load theory "Transcendence_Series_Hancl_Rucki.Transcendence_Series" (unresolved "Prime_Number_Theorem.Prime_Number_Theorem_Library")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a<..<?b} - ?S ⟹ (?f has_vector_derivative ?f' x) (at x);
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
Y
At command "by" (line 739 of "~~/dirs/AFP/thys/Euler_MacLaurin/Euler_MacLaurin.thy")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
Timeout
Failed to load theory "Dirichlet_Series.Dirichlet_Series_Analysis" (unresolved "Dirichlet_Series.Partial_Summation")
Failed to load theory "Zeta_Function.Zeta_Library" (unresolved "Dirichlet_Series.Dirichlet_Series_Analysis")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal" (unresolved "Zeta_Function.Zeta_Library")
Failed to load theory "Executable_Randomized_Algorithms.Randomized_Algorithm" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm_Internal")
Failed to load theory "Finite_Fields.Find_Irreducible_Poly" (unresolved "Executable_Randomized_Algorithms.Randomized_Algorithm")
Failed to load theory "Universal_Hash_Families.Pseudorandom_Objects_Hash_Families" (unresolved "Finite_Fields.Find_Irreducible_Poly")
exception THM 0 raised (line 307 of "drule.ML"):
OF: no unifiers
⟦countable ?S; ?a ≤ ?b;
⋀x. x ∈ {?a..?b} - ?S ⟹
(?f has_vector_derivative ?f' x) (at x within {?a..?b});
continuous_on {?a..?b} ?f⟧
⟹ (?f' has_integral ?f ?b - ?f ?a) {?a..?b}
finite
X
At command "by" (line 46 of "~~/dirs/AFP/thys/Dirichlet_Series/Partial_Summation.thy")
Timeout
Timeout
Timeout
Timeout
Compilation failed (line 28 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.thy"):
can't use native codegen on ARM64 target
usage: mlton [option ...] file.{c|mlb|o|sml} [file.{c|o|s|S} ...]
-align {8|4} object alignment
-as-opt <opt> pass option to assembler
-cc <cc> executable for C compiler
-cc-opt <opt> pass option to C compiler
-codegen {c|llvm} which code generator to use
-const '<name> <value>' set compile-time constant
-default-ann <ann> set annotation default for mlb files
-default-type '<ty><N>' set default type
-disable-ann <ann> disable annotation in mlb files
-export-header <file> write C header file for _export's
-ieee-fp {false|true} use strict IEEE floating-point
-inline <n> set inlining threshold
-keep {g|o} save intermediate files
-link-opt <opt> pass option to linker
-llvm-as <llvm-as> executable for llvm .ll -> .bc assembler
-llvm-as-opt <opt> pass option to llvm assembler
-llvm-llc <llc> executable for llvm .bc -> .o system compiler
-llvm-llc-opt <opt> pass option to llvm compiler
-llvm-opt <opt> executable for llvm .bc -> .bc optimizer
-llvm-opt-opt <opt> pass option to llvm optimizer
-mlb-path-map <file> additional MLB path map
-mlb-path-var '<name> <value>' additional MLB path var
-output <file> name of output file
-profile {no|alloc|count|time} produce executable suitable for profiling
-profile-branch {false|true} profile branches in addition to functions
-profile-stack {false|true} profile the stack
-profile-val {false|true} profile val bindings in addition to functions
-runtime <arg> pass arg to runtime via @MLton
-show-basis <file> write final basis environment
-show-def-use <file> write def-use information
-stop {f|g|o|tc} when to stop
-target {self} platform that executable will run on
-target-as-opt <target> <opt> target-dependent assembler option
-target-cc-opt <target> <opt> target-dependent C compiler option
-target-link-opt <target> <opt> target-dependent linker option
-verbose {0|1|2|3} how verbose to be
At command "compile_generated_files" (line 19 of "~~/dirs/AFP/thys/PAC_Checker/PAC_Checker_MLton.thy")
Timeout
Timeout
Timeout
Timeout
Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")
Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script12908996264891165111: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 27 of "~~/src/HOL/Predicate_Compile_Examples/List_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script10566970209931341117: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 82 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script15829659312316453612: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 98 of "~~/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script511787600494737159: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 39 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script7905755439375564824: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 21 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")
Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 98 of "~~/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy")
Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")
Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8204394921566492704: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 98 of "~~/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6653226794459784689: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 27 of "~~/src/HOL/Predicate_Compile_Examples/List_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6872179369787230613: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 154 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script2644322573257342841: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 137 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script10860699580068668238: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 118 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script11653757845729933775: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 105 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script3069558878686844079: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 90 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script11177408745566165759: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 82 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script17665354893790672561: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 162 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script17649280307282304959: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 119 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script12711943566575952201: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 228 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script4246094564990594565: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 220 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script17108465978593326056: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 214 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script1597381407999167018: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 97 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script397503825341365317: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 73 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script17640397014999793687: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 196 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script13949257142685001590: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 195 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script15055016405975047582: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 194 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script9862388941384394929: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 193 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script10317732459044418860: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 39 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script16408892472159639289: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 103 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script16781997458940050097: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 35 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script6976861503908876094: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 25 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script16983851740979935425: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 23 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script15776859329696804946: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 21 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")
Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 98 of "~~/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy")
Failed to load theory "HOL-Imperative_HOL.Imperative_HOL_ex" (unresolved "HOL-Imperative_HOL.Imperative_Quicksort", "HOL-Imperative_HOL.Imperative_Reverse", "HOL-Imperative_HOL.Linked_Lists")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 965 of "~~/src/HOL/Imperative_HOL/ex/Linked_Lists.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 667 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 115 of "~~/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy")
Failed to load theory "HOL-Library.Disjoint_FSets" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Library.Library" (unresolved "HOL-Library.Disjoint_FSets", "HOL-Library.Finite_Map")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script1724896639111706788: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 154 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script7855632443705766374: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 228 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script14712489562837857566: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 196 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script10081085460323793237: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 220 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script12218914112819741112: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 214 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script14059403933271579963: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 194 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script3765950237778159059: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 195 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script7027897768617707135: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 193 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8797299327617438431: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 137 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script12503071431195456342: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 118 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8328495582557106520: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 105 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script15882810047925561720: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 90 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script4560960943214464805: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 82 of "~~/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script14335297388092512251: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 27 of "~~/src/HOL/Predicate_Compile_Examples/List_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script16870847806792042833: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 98 of "~~/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script10578667612800392959: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 162 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script5822644345774346904: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 119 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script7781656625214623357: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 97 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script8175072041683729505: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 73 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script9919236113019922344: line 1: /usr/local/bin/swipl: No such file or directory At command "quickcheck" (line 39 of "~~/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script70119926128893405: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 103 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script1024539430247847750: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 35 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script702652256656208120: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 25 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script16946672764089606742: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 23 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Error caused by prolog system ISABELLE_SWIPL: return code 127 /tmp/isabelle-isatest/bash_script13384184023737108230: line 1: /usr/local/bin/swipl: No such file or directory At command "values_prolog" (line 21 of "~~/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy")
Failed to load theory "HOL-Probability.Fin_Map" (unresolved "HOL-Library.Finite_Map")
Failed to load theory "HOL-Probability.Projective_Limit" (unresolved "HOL-Probability.Fin_Map")
Failed to load theory "HOL-Probability.Probability" (unresolved "HOL-Probability.Projective_Limit")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 1396 of "~~/src/HOL/Library/Finite_Map.thy")
Code check failed for OCaml: "$ISABELLE_OCAMLFIND" ocamlopt -w -p-u -package zarith -linkpkg ROOT.ml At command "export_code" (line 98 of "~~/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy")
Failed to load theory "HOL.Argo" (unresolved "HOL.HOL")
Failed to load theory "HOL.SAT" (unresolved "HOL.Argo")
Failed to load theory "HOL.Ctr_Sugar" (unresolved "HOL.HOL")
Failed to load theory "HOL.Orderings" (unresolved "HOL.HOL")
Failed to load theory "HOL.Groups" (unresolved "HOL.Orderings")
Failed to load theory "HOL.Lattices" (unresolved "HOL.Groups")
Failed to load theory "HOL.Boolean_Algebras" (unresolved "HOL.Lattices")
Failed to load theory "HOL.Set" (unresolved "HOL.Boolean_Algebras", "HOL.Lattices")
Failed to load theory "HOL.Fun" (unresolved "HOL.Set")
Failed to load theory "HOL.Typedef" (unresolved "HOL.Set")
Failed to load theory "HOL.Complete_Lattices" (unresolved "HOL.Fun")
Failed to load theory "HOL.Rings" (unresolved "HOL.Fun", "HOL.Groups", "HOL.Set")
Failed to load theory "HOL.Inductive" (unresolved "HOL.Complete_Lattices", "HOL.Ctr_Sugar")
Failed to load theory "HOL.Product_Type" (unresolved "HOL.Fun", "HOL.Inductive", "HOL.Typedef")
Failed to load theory "HOL.Complete_Partial_Order" (unresolved "HOL.Product_Type")
Failed to load theory "HOL.Nat" (unresolved "HOL.Fun", "HOL.Inductive", "HOL.Rings", "HOL.Typedef")
Failed to load theory "HOL.Sum_Type" (unresolved "HOL.Fun", "HOL.Inductive", "HOL.Typedef")
Failed to load theory "HOL.Meson" (unresolved "HOL.Nat")
Failed to load theory "HOL.Fields" (unresolved "HOL.Nat")
Failed to load theory "HOL.Relation" (unresolved "HOL.Fields", "HOL.Product_Type", "HOL.Sum_Type")
Failed to load theory "HOL.Finite_Set" (unresolved "HOL.Fields", "HOL.Product_Type", "HOL.Relation", "HOL.Sum_Type")
Failed to load theory "HOL.Transitive_Closure" (unresolved "HOL.Finite_Set")
Failed to load theory "HOL.Wellfounded" (unresolved "HOL.Transitive_Closure")
Failed to load theory "HOL.Fun_Def_Base" (unresolved "HOL.Ctr_Sugar", "HOL.Set", "HOL.Wellfounded")
Failed to load theory "HOL.Hilbert_Choice" (unresolved "HOL.Wellfounded")
Failed to load theory "HOL.Wfrec" (unresolved "HOL.Wellfounded")
Failed to load theory "HOL.ATP" (unresolved "HOL.Hilbert_Choice", "HOL.Meson")
Failed to load theory "HOL.Order_Relation" (unresolved "HOL.Wfrec")
Failed to load theory "HOL.Metis" (unresolved "HOL.ATP")
Failed to load theory "HOL.BNF_Wellorder_Relation" (unresolved "HOL.Order_Relation")
Failed to load theory "HOL.Zorn" (unresolved "HOL.Hilbert_Choice", "HOL.Order_Relation")
Failed to load theory "HOL.BNF_Wellorder_Embedding" (unresolved "HOL.BNF_Wellorder_Relation", "HOL.Hilbert_Choice")
Failed to load theory "HOL.BNF_Wellorder_Constructions" (unresolved "HOL.BNF_Wellorder_Embedding")
Failed to load theory "HOL.BNF_Cardinal_Order_Relation" (unresolved "HOL.BNF_Wellorder_Constructions", "HOL.Zorn")
Failed to load theory "HOL.BNF_Cardinal_Arithmetic" (unresolved "HOL.BNF_Cardinal_Order_Relation")
Failed to load theory "HOL.BNF_Def" (unresolved "HOL.BNF_Cardinal_Arithmetic", "HOL.Fun_Def_Base")
Failed to load theory "HOL.BNF_Composition" (unresolved "HOL.BNF_Def")
Failed to load theory "HOL.Basic_BNFs" (unresolved "HOL.BNF_Def")
Failed to load theory "HOL.BNF_Fixpoint_Base" (unresolved "HOL.BNF_Composition", "HOL.Basic_BNFs")
Failed to load theory "HOL.BNF_Least_Fixpoint" (unresolved "HOL.BNF_Fixpoint_Base")
Failed to load theory "HOL.Basic_BNF_LFPs" (unresolved "HOL.BNF_Least_Fixpoint")
Failed to load theory "HOL.Equiv_Relations" (unresolved "HOL.BNF_Least_Fixpoint")
Failed to load theory "HOL.Transfer" (unresolved "HOL.Basic_BNF_LFPs", "HOL.Hilbert_Choice", "HOL.Metis")
Failed to load theory "HOL.Num" (unresolved "HOL.BNF_Least_Fixpoint", "HOL.Transfer")
Failed to load theory "HOL.Lifting" (unresolved "HOL.Equiv_Relations", "HOL.Transfer")
Failed to load theory "HOL.Power" (unresolved "HOL.Num")
Failed to load theory "HOL.Groups_Big" (unresolved "HOL.Equiv_Relations", "HOL.Power")
Failed to load theory "HOL.Option" (unresolved "HOL.Lifting")
Failed to load theory "HOL.Quotient" (unresolved "HOL.Lifting")
Failed to load theory "HOL.Lifting_Set" (unresolved "HOL.Groups_Big", "HOL.Lifting")
Failed to load theory "HOL.Extraction" (unresolved "HOL.Option")
Failed to load theory "HOL.Partial_Function" (unresolved "HOL.Complete_Partial_Order", "HOL.Option")
Failed to load theory "HOL.Lattices_Big" (unresolved "HOL.Groups_Big", "HOL.Option")
Failed to load theory "HOL.Fun_Def" (unresolved "HOL.Basic_BNF_LFPs", "HOL.Partial_Function", "HOL.SAT")
Failed to load theory "HOL.Int" (unresolved "HOL.Fun_Def", "HOL.Groups_Big", "HOL.Quotient")
Failed to load theory "HOL.Euclidean_Rings" (unresolved "HOL.Int", "HOL.Lattices_Big")
Failed to load theory "HOL.Parity" (unresolved "HOL.Euclidean_Rings")
Failed to load theory "HOL.Numeral_Simprocs" (unresolved "HOL.Parity")
Failed to load theory "HOL.Set_Interval" (unresolved "HOL.Parity")
Failed to load theory "HOL.SMT" (unresolved "HOL.Numeral_Simprocs")
Failed to load theory "HOL.Semiring_Normalization" (unresolved "HOL.Numeral_Simprocs")
Failed to load theory "HOL.Groebner_Basis" (unresolved "HOL.Parity", "HOL.Semiring_Normalization")
Failed to load theory "HOL.Conditionally_Complete_Lattices" (unresolved "HOL.Finite_Set", "HOL.Lattices_Big", "HOL.Set_Interval")
Failed to load theory "HOL.Filter" (unresolved "HOL.Lifting_Set", "HOL.Set_Interval")
Failed to load theory "HOL.Presburger" (unresolved "HOL.Groebner_Basis", "HOL.Set_Interval")
Failed to load theory "HOL.Try0_HOL" (unresolved "HOL.Presburger")
Failed to load theory "HOL.Sledgehammer" (unresolved "HOL.Presburger", "HOL.SMT", "HOL.Try0_HOL")
Failed to load theory "HOL.List" (unresolved "HOL.Lifting_Set", "HOL.Sledgehammer")
Failed to load theory "HOL.Groups_List" (unresolved "HOL.List")
Failed to load theory "HOL.Bit_Operations" (unresolved "HOL.Groups_List", "HOL.Presburger")
Failed to load theory "HOL.Factorial" (unresolved "HOL.Groups_List")
Failed to load theory "HOL.Code_Numeral" (unresolved "HOL.Bit_Operations", "HOL.Lifting")
Failed to load theory "HOL.Map" (unresolved "HOL.List")
Failed to load theory "HOL.Binomial" (unresolved "HOL.Factorial", "HOL.Presburger")
Failed to load theory "HOL.GCD" (unresolved "HOL.Code_Numeral", "HOL.Groups_List")
Failed to load theory "HOL.Enum" (unresolved "HOL.Groups_List", "HOL.Map")
Failed to load theory "HOL.Random" (unresolved "HOL.Code_Numeral", "HOL.Groups_List", "HOL.List")
Failed to load theory "HOL.String" (unresolved "HOL.Bit_Operations", "HOL.Code_Numeral", "HOL.Enum")
Failed to load theory "HOL.BNF_Greatest_Fixpoint" (unresolved "HOL.BNF_Fixpoint_Base", "HOL.String")
Failed to load theory "HOL.Predicate" (unresolved "HOL.String")
Failed to load theory "HOL.Typerep" (unresolved "HOL.String")
Failed to load theory "HOL.Lazy_Sequence" (unresolved "HOL.Predicate")
Failed to load theory "HOL.Limited_Sequence" (unresolved "HOL.Lazy_Sequence")
Failed to load theory "HOL.Code_Evaluation" (unresolved "HOL.Limited_Sequence", "HOL.Typerep")
Failed to load theory "HOL.Quickcheck_Random" (unresolved "HOL.Code_Evaluation", "HOL.Enum", "HOL.Random")
Failed to load theory "HOL.Quickcheck_Exhaustive" (unresolved "HOL.Quickcheck_Random")
Failed to load theory "HOL.Record" (unresolved "HOL.Quickcheck_Exhaustive")
Failed to load theory "HOL.Nitpick" (unresolved "HOL.GCD", "HOL.Record")
Failed to load theory "HOL.Nunchaku" (unresolved "HOL.Nitpick")
Failed to load theory "HOL.Quickcheck_Narrowing" (unresolved "HOL.Quickcheck_Random")
Failed to load theory "HOL.Random_Pred" (unresolved "HOL.Quickcheck_Random")
Failed to load theory "HOL.Random_Sequence" (unresolved "HOL.Random_Pred")
Failed to load theory "HOL.Predicate_Compile" (unresolved "HOL.Quickcheck_Exhaustive", "HOL.Random_Sequence")
Failed to load theory "HOL.Mirabelle" (unresolved "HOL.Predicate_Compile", "HOL.Presburger", "HOL.Sledgehammer")
Failed to load theory "Main" (unresolved "HOL.BNF_Greatest_Fixpoint", "HOL.Binomial", "HOL.Conditionally_Complete_Lattices", "HOL.Extraction", "HOL.Filter", "HOL.GCD", "HOL.Mirabelle", "HOL.Nunchaku", "HOL.Predicate_Compile", "HOL.Quickcheck_Narrowing")
Failed to load theory "HOL.Archimedean_Field" (unresolved "Main")
Failed to load theory "HOL.Rat" (unresolved "HOL.Archimedean_Field")
Failed to load theory "HOL.Real" (unresolved "HOL.Rat")
Failed to load theory "HOL.Hull" (unresolved "Main")
Failed to load theory "HOL.Topological_Spaces" (unresolved "Main")
Failed to load theory "HOL.Binomial_Plus" (unresolved "HOL.Real")
Failed to load theory "HOL.Modules" (unresolved "HOL.Hull")
Failed to load theory "HOL.Vector_Spaces" (unresolved "HOL.Modules")
Failed to load theory "HOL.Real_Vector_Spaces" (unresolved "HOL.Real", "HOL.Topological_Spaces", "HOL.Vector_Spaces")
Failed to load theory "HOL.Inequalities" (unresolved "HOL.Real_Vector_Spaces")
Failed to load theory "HOL.Limits" (unresolved "HOL.Real_Vector_Spaces")
Failed to load theory "HOL.Deriv" (unresolved "HOL.Limits")
Failed to load theory "HOL.Series" (unresolved "HOL.Inequalities", "HOL.Limits")
Failed to load theory "HOL.NthRoot" (unresolved "HOL.Deriv")
Failed to load theory "HOL.Transcendental" (unresolved "HOL.Deriv", "HOL.NthRoot", "HOL.Series")
Failed to load theory "HOL.Complex" (unresolved "HOL.Real_Vector_Spaces", "HOL.Transcendental")
Failed to load theory "HOL.MacLaurin" (unresolved "HOL.Transcendental")
Failed to load theory "Complex_Main" (unresolved "HOL.Binomial_Plus", "HOL.Complex", "HOL.MacLaurin")
Cheating requires interactive or quick_and_dirty mode! At command "ML_file" (line 797 of "~~/src/HOL/HOL.thy")
Cheating requires interactive or quick_and_dirty mode! At command "by" (line 16 of "~~/src/Pure/ex/Guess_Examples.thy")
Failed to load theory "ZF.IntDiv" (unresolved "ZF.Bin")
Failed to load theory "ZF" (unresolved "ZF.IntDiv")
Failed to load theory "ZF.AC" (unresolved "ZF")
Failed to load theory "ZF.Zorn" (unresolved "ZF.AC")
Failed to load theory "ZF.Cardinal_AC" (unresolved "ZF.Zorn")
Failed to load theory "ZF.InfDatatype" (unresolved "ZF.Cardinal_AC")
Failed to load theory "ZFC" (unresolved "ZF", "ZF.InfDatatype")
Cheating requires interactive or quick_and_dirty mode! At command "ML_file" (line 706 of "~~/src/ZF/Bin.thy")