indrule.ML
changeset 136 0a43cf458998
parent 128 89669c58e506
child 140 f745ff8bdb91
--- 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*)