src/LCF/ex/Ex2.ML
author wenzelm
Mon Jun 22 15:09:59 1998 +0200 (1998-06-22)
changeset 5061 f947332d5465
parent 4905 be73ddff6c5a
child 17878 5b9efe4d6b47
permissions -rw-r--r--
isatool fixgoal;
wenzelm@4905
     1
wenzelm@4905
     2
simpset_ref() := LCF_ss;
wenzelm@4905
     3
wenzelm@4905
     4
Addsimps [F_strict,K];
wenzelm@4905
     5
wenzelm@5061
     6
Goal "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
wenzelm@4905
     7
by (stac H 1);
wenzelm@4905
     8
by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
wenzelm@4905
     9
by (Simp_tac 1);
wenzelm@4905
    10
by (asm_simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
wenzelm@4905
    11
qed "example";