Mercurial Mercurial > hg > nominal2 / 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.
merged
authorChristian Urban <urbanc@in.tum.de>
Tue, 01 May 2012 12:16:04 +0100
changeset 3166 51c475ceaf09
parent 3165 31c64dd4c95a (diff)
parent 3164 25c61cc06ae2 (current diff)
child 3167 c25386402f6a
merged
--- a/Nominal/nominal_function.ML	Fri Apr 20 18:58:03 2012 +0200
+++ b/Nominal/nominal_function.ML	Tue May 01 12:16:04 2012 +0100
@@ -245,7 +245,6 @@
     (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
     "declaration of congruence rule for function definitions"
   #> setup_case_cong
-  #> Function_Relation.setup
   #> Function_Common.Termination_Simps.setup
 
 val get_congs = Function_Ctx_Tree.get_function_congs
nominal2