src/LCF/ex/Ex2.ML
author wenzelm
Fri, 15 May 1998 11:34:12 +0200
changeset 4932 c90411dde8e8
parent 4905 be73ddff6c5a
child 5061 f947332d5465
permissions -rw-r--r--
PureThy.add_typedecls;


simpset_ref() := LCF_ss;

Addsimps [F_strict,K];

goal thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
by (stac H 1);
by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
qed "example";