--- a/indrule.ML Tue Sep 06 10:56:54 1994 +0200
+++ b/indrule.ML Tue Sep 06 13:24:29 1994 +0200
@@ -90,8 +90,8 @@
(*** Prove the simultaneous induction rule ***)
-(*Make distinct predicates for each inductive set;
- Cartesian products in domT should nest ONLY to the left! *)
+(*Make distinct predicates for each inductive set.
+ Splits cartesian products in domT, IF nested to the right! *)
(*Given a recursive set and its domain, return the "split" predicate
and a conclusion for the simultaneous induction rule*)