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.
adapted Function_Lib (cf. b8cdd3d73022);
authorwenzelm
Sun, 25 Oct 2009 00:00:53 +0200
changeset 33102 e3463e6db704
parent 33101 8846318b52d0
child 33103 9d7d0bef2a77
adapted Function_Lib (cf. b8cdd3d73022);
src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions
src/HOL/SizeChange/sct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Multiset.thy	Sat Oct 24 20:47:10 2009 +0200
+++ b/src/HOL/Library/Multiset.thy	Sun Oct 25 00:00:53 2009 +0200
@@ -1607,7 +1607,7 @@
       rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
 
   val regroup_munion_conv =
-      FundefLib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
+      Function_Lib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
         (map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp}))
 
   fun unfold_pwleq_tac i =
--- a/src/HOL/SizeChange/sct.ML	Sat Oct 24 20:47:10 2009 +0200
+++ b/src/HOL/SizeChange/sct.ML	Sun Oct 25 00:00:53 2009 +0200
@@ -112,7 +112,7 @@
     end
 
 fun bind_many [] = I
-  | bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
+  | bind_many vs = Function_Lib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
 
 (* Builds relation descriptions from a relation definition *)
 fun mk_reldescs (Abs a) =
isabelle