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.
Equivariance prover now uses permutation simprocs as well.
authorberghofe
Thu, 20 Mar 2008 16:28:23 +0100
changeset 26364 cb6f360ab425
parent 26363 9d95309f8069
child 26365 e6d3714b8853
Equivariance prover now uses permutation simprocs as well.
src/HOL/Nominal/nominal_inductive.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 16:04:34 2008 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 20 16:28:23 2008 +0100
@@ -605,9 +605,10 @@
          atoms)
       end;
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
-    val eqvt_ss = HOL_basic_ss addsimps
+    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps
       (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
-      [mk_perm_bool_simproc names];
+      [mk_perm_bool_simproc names,
+       NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
     val t = Logic.unvarify (concl_of raw_induct);
     val pi = Name.variant (add_term_names (t, [])) "pi";
     val ps = map (fst o HOLogic.dest_imp)
isabelle