[isabelle] Isabelle2014-RC1: Completion of qualified fact names
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Isabelle2014-RC1: Completion of qualified fact names
- From: Lars Hupel <hupel at in.tum.de>
- Date: Thu, 31 Jul 2014 10:16:45 +0200
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.6.0
assume this simple inductive definition:
inductive foo :: "nat ⇒ bool" where
foo1: "foo 0"
Now, trying the completion:
... this gives me "foo.cases", "foo.induct", ... (as expected), and also
"foo1". It doesn't give me "foo.foo1", though.
Peter suggested that the general policy seems to be that if the short
name is in scope, the longer name gets filtered out. Adding another
inductive which introduces another "foo1" rule confirms that observation.
inductive foo2 :: "nat ⇒ bool" where
foo1: "foo2 0"
... now has "foo.foo1", but not "foo2.foo1".
Could this be changed or configurable? Sometimes, it is preferable to
give the long names, even if the shorter ones are in scope.
Side note: Pressing <Ctrl-B> after "thm foo." (notice the dot) doesn't
open the completion dialog.
This archive was generated by a fusion of
Pipermail (Mailman edition) and