changeset 4905 | be73ddff6c5a |
child 5061 | f947332d5465 |
4904:5f6b2dd1cd11 | 4905:be73ddff6c5a |
---|---|
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"; |