# HG changeset patch # User nipkow # Date 785766807 -3600 # Node ID d5c6d1fb236b2bb1823b62318ce22aed7a25d8ba # Parent 3f5136a61a72f114495ee5a1dab7df72be4a4c4e removed Sum-rules diff -r 3f5136a61a72 -r d5c6d1fb236b ind_syntax.ML --- a/ind_syntax.ML Fri Nov 25 11:10:26 1994 +0100 +++ b/ind_syntax.ML Fri Nov 25 13:33:27 1994 +0100 @@ -136,7 +136,7 @@ (*For simplifying the elimination rule*) val sumprod_free_SEs = Pair_inject :: - map make_elim [Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject]; + map make_elim [(*Inl_neq_Inr, Inr_neq_Inl, Inl_inject, Inr_inject*)]; (*For deriving cases rules. read_instantiate replaces a propositional variable by a formula variable*)