src/LCF/ex/Ex2.ML

--- a/src/LCF/ex/Ex2.ML	Thu Jun 01 14:54:44 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-
-(* $Id$ *)
-
-Addsimps [F_strict,K];
-
-Goal "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";