Stream: Beginner Questions

Topic: How can the theory name be omitted?

view this post on Zulip Jiekai (Apr 23 2022 at 08:51):

Hello, I'm reading Concrete Semantics.

proof (prove)
goal (2 subgoals):
 1. t2.rev (t2.rev t2.list.Nil) = t2.list.Nil
 2. ⋀x1 xs.
       t2.rev (t2.rev xs) = xs ⟹
       t2.rev (t2.rev (t2.list.Cons x1 xs)) =
       t2.list.Cons x1 xs

My file name is t2. I'm wondering how can the t2 part be omitted in the jEdit State.

view this post on Zulip Mete Polat (Apr 23 2022 at 09:07):

You can use the declare [[names_short]] command to shorten all subsequent lemmas.

Last updated: Jul 15 2022 at 23:21 UTC