[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

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 MHonArc.