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.
inf_fun_eq and inf_bool_eq now with meta equality
authorhaftmann
Fri, 16 Mar 2007 21:32:18 +0100
changeset 22460 b4f96f343d6c
parent 22459 8469640e1489
child 22461 052cfe1c86dc
inf_fun_eq and inf_bool_eq now with meta equality
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Fri Mar 16 21:32:15 2007 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 16 21:32:18 2007 +0100
@@ -533,7 +533,7 @@
         [rewrite_goals_tac [inductive_conj_def],
          DETERM (rtac raw_fp_induct 1),
          REPEAT (resolve_tac [le_funI, le_boolI] 1),
-         rewrite_goals_tac (map mk_meta_eq [inf_fun_eq, inf_bool_eq] @ simp_thms'),
+         rewrite_goals_tac (inf_fun_eq :: inf_bool_eq :: simp_thms'),
          (*This disjE separates out the introduction rules*)
          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
          (*Now break down the individual cases.  No disjE here in case
isabelle