took out legacy material from 'HOL/Library/Library.thy'
authorblanchet
Mon Sep 01 16:17:46 2014 +0200 (2014-09-01)
changeset 58110019c0211ed1f
parent 58109 6d4695335d41
child 58111 82db9ad610b9
took out legacy material from 'HOL/Library/Library.thy'
src/HOL/Library/Library.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Library/Library.thy	Mon Sep 01 16:17:46 2014 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Mon Sep 01 16:17:46 2014 +0200
     1.3 @@ -40,7 +40,6 @@
     1.4    Multiset
     1.5    Numeral_Type
     1.6    NthRoot_Limits
     1.7 -  Old_SMT
     1.8    OptionalSugar
     1.9    Option_ord
    1.10    Order_Continuity
     2.1 --- a/src/HOL/ROOT	Mon Sep 01 16:17:46 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Mon Sep 01 16:17:46 2014 +0200
     2.3 @@ -52,6 +52,7 @@
     2.4      (*legacy tools*)
     2.5      Refute
     2.6      Old_Recdef
     2.7 +    Old_SMT
     2.8    theories [condition = ISABELLE_FULL_TEST]
     2.9      Sum_of_Squares_Remote
    2.10    document_files "root.bib" "root.tex"