src/HOL/Library/Library.thy
changeset 44013 5cfc1c36ae97
parent 43976 af17d7934116
child 44014 88bd7d74a2c1
     1.1 --- a/src/HOL/Library/Library.thy	Tue Aug 02 10:03:14 2011 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Tue Aug 02 10:36:50 2011 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    Multiset
     1.5    Nested_Environment
     1.6    Numeral_Type
     1.7 +  Old_Recdef
     1.8    OptionalSugar
     1.9    Option_ord
    1.10    Permutation