NEWS
changeset 55143 04448228381d
parent 55139 4d899933a51a
child 55152 a56099a6447a
equal deleted inserted replaced
55142:378ae9e46175 55143:04448228381d
    37 process, without requiring old-fashioned command-line invocation of
    37 process, without requiring old-fashioned command-line invocation of
    38 "isabelle jedit -m MODE".
    38 "isabelle jedit -m MODE".
    39 
    39 
    40 
    40 
    41 *** Pure ***
    41 *** Pure ***
       
    42 
       
    43 * Attributes "where" and "of" allow an optional context of local
       
    44 variables ('for' declaration): these variables become schematic in the
       
    45 instantiated theorem.
    42 
    46 
    43 * More thorough check of proof context for goal statements and
    47 * More thorough check of proof context for goal statements and
    44 attributed fact expressions (concerning background theory, declared
    48 attributed fact expressions (concerning background theory, declared
    45 hyps).  Potential INCOMPATIBILITY, tools need to observe standard
    49 hyps).  Potential INCOMPATIBILITY, tools need to observe standard
    46 context discipline.  See also Assumption.add_assumes and the more
    50 context discipline.  See also Assumption.add_assumes and the more
   266     explicit set-comprehensions with eucl_less for other (half-) open
   270     explicit set-comprehensions with eucl_less for other (half-) open
   267     intervals.
   271     intervals.
   268 
   272 
   269 
   273 
   270 *** ML ***
   274 *** ML ***
       
   275 
       
   276 * Proper context discipline for read_instantiate and instantiate_tac:
       
   277 variables that are meant to become schematic need to be given as
       
   278 fixed, and are generalized by the explicit context of local variables.
       
   279 This corresponds to Isar attributes "where" and "of" with 'for'
       
   280 declaration.  INCOMPATIBILITY, also due to potential change of indices
       
   281 of schematic variables.
   271 
   282 
   272 * Toplevel function "use" refers to raw ML bootstrap environment,
   283 * Toplevel function "use" refers to raw ML bootstrap environment,
   273 without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
   284 without Isar context nor antiquotations.  Potential INCOMPATIBILITY.
   274 Note that 'ML_file' is the canonical command to load ML files into the
   285 Note that 'ML_file' is the canonical command to load ML files into the
   275 formal context.
   286 formal context.