NEWS
changeset 29861 3c348f5873f3
parent 29823 0ab754d13ccd
child 29862 d203e9d4675b
equal deleted inserted replaced
29860:f735e4027656 29861:3c348f5873f3
   180 
   180 
   181 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
   181 * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
   182 
   182 
   183 * The 'axiomatization' command now only works within a global theory
   183 * The 'axiomatization' command now only works within a global theory
   184 context.  INCOMPATIBILITY.
   184 context.  INCOMPATIBILITY.
       
   185 
       
   186 * New find_theorems criterion "solves" matching theorems that 
       
   187   directly solve the current goal. Try "find_theorm solves".
       
   188 
       
   189 * Added an auto solve option, which can be enabled through the
       
   190   ProofGeneral Isabelle settings menu (disabled by default).
       
   191  
       
   192   When enabled, find_theorems solves is called whenever a new lemma
       
   193   is stated. Any theorems that could solve the lemma directly are
       
   194   listed underneath the goal.
   185 
   195 
   186 
   196 
   187 *** Document preparation ***
   197 *** Document preparation ***
   188 
   198 
   189 * Antiquotation @{lemma} now imitates a regular terminal proof,
   199 * Antiquotation @{lemma} now imitates a regular terminal proof,