Email Gateway (Aug 18 2022 at 16:45): Email Gateway (Aug 18 2022 at 16:45):From: Victor Porton <porton@narod.ru>
The below theory does not verify. I need to know what is my error.
theory test
imports Main_ZF
begin
lemma "ALL a:big. ALL b:big. movea = moveb --> a=b"
proof
{
fix "a" "b"
assume "a: big" "b: big"
have "movea = moveb --> a=b" sorry
}
thus ?thesis by blast
qed
end
(It is important that you'd help me because after solving this issue I will be
near to create an important new theory for ZF which formalizes the concept of
generalization. This theory will influence Isabelle much, even despite of I'm
a very novice theory writer. So please HELP me to pass this step.)
\--
Victor Porton - http://portonvictor.org
Last updated: Nov 21 2024 at 12:39 UTC