1
2
simpset_ref() := LCF_ss;
3
4
Addsimps [F_strict,K];
5
6
Goal "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
7
by (stac H 1);
8
by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
9
by (Simp_tac 1);
10
by (asm_simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
11
qed "example";