Mercurial Mercurial > repos > Old_HOL / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed Sum-rules
authornipkow
Fri, 25 Nov 1994 13:33:27 +0100
changeset 182 d5c6d1fb236b
parent 181 3f5136a61a72
child 183 74ce9774c923
removed Sum-rules
ind_syntax.ML file | annotate | diff | comparison | revisions 
--- 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*)
Old_HOL