4905
|
1 |
|
|
2 |
simpset_ref() := LCF_ss;
|
|
3 |
|
|
4 |
Addsimps [F_strict,K];
|
|
5 |
|
|
6 |
goal thy "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";
|