Stream: Beginner Questions

Topic: ✔ How can the theory name be omitted?

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.

Mete Polat (Apr 23 2022 at 09:07):

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

Notification Bot (Apr 23 2022 at 09:20):

Jiekai has marked this topic as resolved.

Last updated: Dec 21 2024 at 16:20 UTC