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.
You can use the
declare [[names_short]] command to shorten all subsequent lemmas.
Last updated: Jul 15 2022 at 23:21 UTC