Mercurial Mercurial > repos > isabelle / 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.
Replaced Nat.thy by NatDef.thy because Nat.thy depends on
authorberghofe
Fri, 24 Jul 1998 12:53:04 +0200
changeset 5179 819f90f278db
parent 5178 9337b230ff15
child 5180 d82a70766af0
Replaced Nat.thy by NatDef.thy because Nat.thy depends on inductive_package.
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Fri Jul 24 12:50:34 1998 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 24 12:53:04 1998 +0200
@@ -288,7 +288,7 @@
 fun con_elim_tac simps =
   let val elim_tac = REPEAT o (eresolve_tac elim_rls)
   in ALLGOALS(EVERY'[elim_tac,
-                 asm_full_simp_tac (simpset_of Nat.thy addsimps simps),
+                 asm_full_simp_tac (simpset_of NatDef.thy addsimps simps),
                  elim_tac,
                  REPEAT o bound_hyp_subst_tac])
      THEN prune_params_tac
isabelle