[isabelle] Trouble with raw proof blocks



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. move`a = move`b --> a=b"
proof
  {
    fix "a" "b"
    assume "a: big" "b: big"
    have "move`a = move`b --> 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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.