Hi guys, can anyone explain about what is the difference between imports "geometry_theory" and imports geometry_theory. What is the meaning of using quotation mark here?
sometimes the quotes are necessary if the theory you're importing contains some special characters, such as
However you need the quotations marks if the name contains an hyphen, like
(Also, the Isabelle convention is to capitalise theory names like
you are right
shouldn't the goal be solved directly by the two assumptions?
I struggle understanding the current "problem" :-)
using this: ?x ∈ E ⟹ t ?x = Some ?y ⟶ ?y ∈ V ?x ∉ E ⟹ t ?x = None goal (1 subgoal): 1. ran t = V
Last updated: Jul 15 2022 at 23:21 UTC