isabelle: src/LCF/ex/Ex2.ML@05fc32a23b8b (annotated)

4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	1
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	2	simpset_ref() := LCF_ss;
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	3
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	4	Addsimps [F_strict,K];
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	5
5061 f947332d5465 isatool fixgoal; wenzelm parents: 4905 diff changeset	6	Goal "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
4905 be73ddff6c5a proper thy files; wenzelm parents: diff changeset	7	by (stac H 1);
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	8	by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	9	by (Simp_tac 1);
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	10	by (asm_simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
be73ddff6c5a proper thy files; wenzelm parents: diff changeset	11	qed "example";