Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/intr-elim.ML
changeset 70 8a29f8b4aca1
parent 55 331d93292ee0 
--- a/src/ZF/intr-elim.ML	Fri Oct 22 11:25:15 1993 +0100
+++ b/src/ZF/intr-elim.ML	Fri Oct 22 11:34:41 1993 +0100
@@ -263,8 +263,8 @@
 
 (*Includes rules for succ and Pair since they are common constructions*)
 val elim_rls = [asm_rl, FalseE, succ_neq_0, sym RS succ_neq_0, 
-		Pair_neq_0, sym RS Pair_neq_0, succ_inject, refl_thin,
-		conjE, exE, disjE];
+		Pair_neq_0, sym RS Pair_neq_0, make_elim succ_inject, 
+		refl_thin, conjE, exE, disjE];
 
 val sumprod_free_SEs = 
     map (gen_make_elim [conjE,FalseE])
@@ -283,7 +283,7 @@
   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   for inference systems. *)
 fun con_elim_tac defs =
-    rewrite_goals_tac defs THEN basic_elim_tac THEN fold_con_tac defs;
+    rewrite_goals_tac defs THEN basic_elim_tac THEN fold_tac defs;
 
 (*String s should have the form t:Si where Si is an inductive set*)
 fun mk_cases defs s =
isabelle