diff -r d3fcc1a0272c -r 90bee31628dc CookBook/infix_conv.ML
--- a/CookBook/infix_conv.ML	Thu Feb 26 13:46:05 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-signature INFIX_CONV =
-sig
-  val then_conv : Thm.conv * Thm.conv -> Thm.conv
-  val else_conv : Thm.conv * Thm.conv -> Thm.conv
-end
-
-structure InfixConv : INFIX_CONV = Conv
-
-open InfixConv