renamed NamedThmsFun to Named_Thms;
authorwenzelm
Thu Jul 02 17:33:36 2009 +0200 (2009-07-02)
changeset 31901e280491f36b8
parent 31900 7c35d9ad0349
child 31902 862ae16a799d
renamed NamedThmsFun to Named_Thms;
NEWS
src/Pure/Tools/named_thms.ML
     1.1 --- a/NEWS	Thu Jul 02 17:30:54 2009 +0200
     1.2 +++ b/NEWS	Thu Jul 02 17:33:36 2009 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4  boundaries of intervals and implements interval splitting and Taylor
     1.5  series expansion.
     1.6  
     1.7 -* Changed DERIV_intros to a dynamic fact (via NamedThmsFun).  Each of
     1.8 +* Changed DERIV_intros to a dynamic fact (via Named_Thms).  Each of
     1.9  the theorems in DERIV_intros assumes composition with an additional
    1.10  function and matches a variable to the derivative, which has to be
    1.11  solved by the simplifier.  Hence (auto intro!: DERIV_intros) computes
    1.12 @@ -92,6 +92,8 @@
    1.13  
    1.14  *** ML ***
    1.15  
    1.16 +* Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
    1.17 +
    1.18  * Eliminated old Attrib.add_attributes, Method.add_methods and related
    1.19  cominators for "args".  INCOMPATIBILITY, need to use simplified
    1.20  Attrib/Method.setup introduced in Isabelle2009.
     2.1 --- a/src/Pure/Tools/named_thms.ML	Thu Jul 02 17:30:54 2009 +0200
     2.2 +++ b/src/Pure/Tools/named_thms.ML	Thu Jul 02 17:33:36 2009 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4    val setup: theory -> theory
     2.5  end;
     2.6  
     2.7 -functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
     2.8 +functor Named_Thms(val name: string val description: string): NAMED_THMS =
     2.9  struct
    2.10  
    2.11  structure Data = GenericDataFun