--- a/src/HOL/Matrix/conv.ML Mon Mar 07 16:55:36 2005 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-exception Fail_conv;
-
-fun orelsec conv1 conv2 ct = conv1 ct handle Fail_conv => conv2 ct
-
-val allc = Thm.reflexive
-
-fun thenc conv1 conv2 ct =
- let
- fun rhs_of t = snd (Thm.dest_comb (strip_imp_concl (cprop_of t)))
-
- val eq = conv1 ct
- in
- Thm.transitive eq (conv2 (rhs_of eq))
- end
-
-fun subc conv ct =
- case term_of ct of
- _ $ _ =>
- let
- val (ct1, ct2) = Thm.dest_comb ct
- in
- Thm.combination (conv ct1) (conv ct2)
- end
- | _ => allc ct
-
-fun botc conv ct = thenc (subc (botc conv)) (orelsec conv allc) ct
\ No newline at end of file