--- a/src/HOL/IsaMakefile Fri Jan 06 11:15:02 2012 +0100
+++ b/src/HOL/IsaMakefile Fri Jan 06 20:39:50 2012 +0100
@@ -286,7 +286,6 @@
List.thy \
Main.thy \
Map.thy \
- More_List.thy \
More_Set.thy \
Nat_Numeral.thy \
Nat_Transfer.thy \
--- a/src/HOL/Library/Monad_Syntax.thy Fri Jan 06 11:15:02 2012 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy Fri Jan 06 20:39:50 2012 +0100
@@ -74,7 +74,7 @@
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
#> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
- #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
+ #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
*}
end
--- a/src/HOL/List.thy Fri Jan 06 11:15:02 2012 +0100
+++ b/src/HOL/List.thy Fri Jan 06 20:39:50 2012 +0100
@@ -5109,6 +5109,19 @@
by (induct xs) force+
+subsection {* Monad operation *}
+
+definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
+ "bind xs f = concat (map f xs)"
+
+hide_const (open) bind
+
+lemma bind_simps [simp]:
+ "List.bind [] f = []"
+ "List.bind (x # xs) f = f x @ List.bind xs f"
+ by (simp_all add: bind_def)
+
+
subsection {* Transfer *}
definition
--- a/src/HOL/More_List.thy Fri Jan 06 11:15:02 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Operations on lists beyond the standard List theory *}
-
-theory More_List
-imports List
-begin
-
-text {* monad operation *}
-
-definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
- "bind xs f = concat (map f xs)"
-
-lemma bind_simps [simp]:
- "bind [] f = []"
- "bind (x # xs) f = f x @ bind xs f"
- by (simp_all add: bind_def)
-
-end
--- a/src/HOL/More_Set.thy Fri Jan 06 11:15:02 2012 +0100
+++ b/src/HOL/More_Set.thy Fri Jan 06 20:39:50 2012 +0100
@@ -4,7 +4,7 @@
header {* Relating (finite) sets and lists *}
theory More_Set
-imports More_List
+imports List
begin
lemma comp_fun_idem_remove: