NEWS
changeset 37868 59eed00bfd8e
parent 37820 ffaca9167c16
child 37939 965537d86fcc
equal deleted inserted replaced
37867:b9783e9e96e1 37868:59eed00bfd8e
    99 INCOMPATIBILITY.
    99 INCOMPATIBILITY.
   100 
   100 
   101 * Inductive package: offers new command "inductive_simps" to automatically
   101 * Inductive package: offers new command "inductive_simps" to automatically
   102   derive instantiated and simplified equations for inductive predicates,
   102   derive instantiated and simplified equations for inductive predicates,
   103   similar to inductive_cases.
   103   similar to inductive_cases.
       
   104 
       
   105 
       
   106 *** ML ***
       
   107 
       
   108 * ML antiquotations @{theory} and @{theory_ref} refer to named
       
   109 theories from the ancestry of the current context, not any accidental
       
   110 theory loader state as before.  Potential INCOMPATIBILITY, subtle
       
   111 change in semantics.
       
   112 
   104 
   113 
   105 
   114 
   106 New in Isabelle2009-2 (June 2010)
   115 New in Isabelle2009-2 (June 2010)
   107 ---------------------------------
   116 ---------------------------------
   108 
   117