Hi I am very much a beginer!
imports HOL.Lattices "HOL-Lattice.Orders" begin
works. But when I run isabelle build it objects to the second import
dstr@D Gal % isabelle build -D PreGalois
*** Cannot load theory "HOL-Lattice.Orders"
Any ideas much appreciated
Given the ROOT file, only the import
HOL_Lattice.CompleteLattice should work
(Orders is transitively included)
The ROOT file includes only one file and this is the only one you should (and can) import:
session "HOL-Lattice" in Lattice = HOL + description " Author: Markus Wenzel, TU Muenchen Basic theory of lattices and orders. " theories CompleteLattice document_files "root.tex"
(jEdit is less strict on those things for some reason)
I am getting their slowly. As Lattice imports Bounds and that imports Orders all I need is
imports "HOL.Lattices" begin
This import works (JEdit) but now the reference to quasi_order that was working (its a class in Orders) breaks
interpretation "abs" : quasi_order "(⊑a) :: 'a ⇒ 'a ⇒ bool"
I have tried Orders_quasi_order , Orders.quasi_order and adding " " but can not find how to reference something thats in a nested import.
HOL-Lattice.CompleteLattice are not the same
Import Main instead of only
Mathias Fleury said:
HOL-Lattice.CompleteLatticeare not the same
To be clear: quasi_order is defined in "~~src/HOL/Lattice/Orders.thy", so you have to import that theory with
HOL-Lattice.CompleteLattice and not
HOL.Lattices refers to "~ ~src/HOL/Lattices.thy", not "~ ~src/HOL/Lattice/<some_theory_here>"
Last updated: Jul 15 2022 at 23:21 UTC