[isabelle] Novice question about functions
I am writing my first real Isabelle theory (indeed very useful for other Isabelle users). I step on the following question.
Let move_fun is an arbitrary function and myset is an arbitrary set (in ZF). How to prove the theorem (marked sorry)?
locale subtest =
definition "move == (lam x:myset. move_fun(x))"
theorem "x: my_set ==> move`x = move_fun(x)" sorry
Victor Porton - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and