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/HOL/Tools/function_package/fundef_package.ML
changeset 26749 397a1aeede7d
parent 26628 63306cb94313
child 26989 9b2acb536228 
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Apr 25 15:30:33 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Apr 25 16:28:06 2008 +0200
@@ -184,6 +184,7 @@
       "declaration of congruence rule for function definitions")]
   #> setup_case_cong
   #> FundefRelation.setup
+  #> FundefCommon.TerminationSimps.setup
 
 val get_congs = FundefCtxTree.get_fundef_congs o Context.Theory
isabelle