src/HOL/Library/Library.thy
changeset 23854 688a8a7bcd4e
parent 23192 ec73b9707d48
child 24197 c9e3cb5e5681
--- a/src/HOL/Library/Library.thy	Thu Jul 19 21:47:38 2007 +0200
+++ b/src/HOL/Library/Library.thy	Thu Jul 19 21:47:39 2007 +0200
@@ -9,15 +9,15 @@
   Coinductive_List
   Commutative_Ring
   Continuity
-  EfficientNat
+  Efficient_Nat
   Eval
-  ExecutableRat
+  Executable_Rat
   Executable_Real
-  ExecutableSet
+  Executable_Set
   FuncSet
   GCD
   Infinite_Set
-  MLString
+  ML_String
   Multiset
   NatPair
   Nat_Infinity