[isabelle] Trouble with raw proof blocks
The below theory does not verify. I need to know what is my error.
lemma "ALL a:big. ALL b:big. move`a = move`b --> a=b"
fix "a" "b"
assume "a: big" "b: big"
have "move`a = move`b --> a=b" sorry
thus ?thesis by blast
(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
This archive was generated by a fusion of
Pipermail (Mailman edition) and