Menu
The following gives bad theory import "Multivariate_Analysis"
imports Multivariate_Analysis
Importing Main works fine, how do I import modules?
276
Isabelle — HOL Clemens Ballarin Hilbert’s Epsilon Operator (David Hilbert, 1862-1943) ε x. P x is a value that satisfies P (if such a value exists) ε also known as description operator. In Isabelle the ε-operator is written SOME x. P x P ?x P (SOME x. P x) someI Isabelle — HOL Clemens Ballarin More Epsilon ε implies Axiom of Choice: ∀x. ∃y.
Isabelle — HOL Clemens Ballarin Type Classes Similar to Haskell’s type classes, but with semantic properties class order = fixes less eq ( infix ” ≤ ” 50) and less ( infix ” < ” 50) assumes order refl: ”x ≤ x” and order trans: ”[[x ≤ y; y ≤ z]] =⇒ x ≤ z” and ... Theorems can be proved in the abstract lemma ( in order) order less trans: ” V x.
P x is a value that satisfies P (if such a value exists) ε also known as description operator. In Isabelle the ε-operator is written SOME x. P x P ?x P (SOME x. P x) someI Isabelle — HOL Clemens Ballarin More Epsilon ε implies Axiom of Choice: ∀x. ∃y. Q x y =⇒ ∃f. ∀x. Q x (f x) Existential and universal quantification can be defined with ε.
For theory imports, you usually have to specify the full or relative path to the theory file. So for Multivariate_Analysis, this is <path to isabelle distrib>/src/HOL/Multivariate_Analysis/Multivariate_Analysis. The path may be only omitted if the theory is already part of the session image. So as Main is part of the default image HOL, you can import it without a path. Opinions diverge whether it is better to import theories from session images with or without paths.
The path may also contain environment variables like $ISABELLE_HOME or $AFP, which users can set in their local settings file such that the theories work across different installations. For everything from the Isabelle distribution, it is custom to use ~~ for the path of the Isabelle distribution folder.
In summary, your import should read as follows:
theory My_Theory
imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
begin
As Multivariate_Analysis is a fairly large module, it might be sensible to change the default session image, though, such that all these theories are not loaded at every start of Isabelle/jEdit afresh. You can do so by specifying -l HOL-Multivariate_Analysis at the command line upon invocation or by selecting this session in the theory panel and restarting Isabelle/jEdit.
Update: Since Isabelle2017, it is preferable to import theories from other sessions via session names instead of relative path names. That is, the
theory Multivariate_Analysis would be imported as
theory My_Theory
imports "HOL-Multivariate_Analysis.Multivariate_Analysis"
begin
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
