(* Title: NSet.ML Date: 2002/10/26 modified 2003/10/31 Author: Jan-Georg Smaus, Universitaet Freiburg Copyright 2003 Universitaet Freiburg *) Goal "(P(t)) \\ (t : { x. P(x) })"; br iffD2 1; br Collect 1; ba 1; qed "inI"; (*an elimination rule as usual in logic*) Goal "(t : { x. P(x) }) \\ P(t)"; br iffD1 1; br Collect 1; ba 1; qed "inElimination"; (*an elimination rule that works with etac*) val [p1,p2] = Goal "\\ (t : { x. P(x) }); P(t) \\ R\\ \\ R"; br p2 1; br inElimination 1; br p1 1; qed "inE"; Goal "(ALL x. x:A \\ x:B) \\ A = B"; br iffD2 1; br ext 1; ba 1; qed "equalsI"; (*an elimination rule as usual in logic*) Goal "A = B \\ (ALL x. x:A \\ x:B)"; br iffD1 1; br ext 1; ba 1; qed "equalsElimination"; (*an elimination rule that works with etac*) val [p1,p2] = Goal "\\ A = B; (ALL x. x:A \\ x:B) \\ R\\ \\ R"; br p2 1; br equalsElimination 1; br p1 1; qed "equalsE";