1
2
(* $Id$ *)
3
4
Addsimps [p_strict,p_s];
5
6
Goal "p(FIX(s),y) = FIX(s)";
7
by (induct_tac "s" 1);
8
by (Simp_tac 1);
9
10
qed "example";