NEWS
changeset 59835 97872c658a44
parent 59815 cce82e360c2f
child 59849 c3d126c7944f
equal deleted inserted replaced
59834:fc3d7eaa486e 59835:97872c658a44
    59 Options / Text Area).
    59 Options / Text Area).
    60 
    60 
    61 
    61 
    62 *** Pure ***
    62 *** Pure ***
    63 
    63 
    64 * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
       
    65 etc.) allow an optional context of local variables ('for' declaration):
       
    66 these variables become schematic in the instantiated theorem. This
       
    67 behaviour is analogous to 'for' in attributes "where" and "of".
       
    68 
       
    69 * Explicit instantiation via attributes "where", "of", and proof methods
    64 * Explicit instantiation via attributes "where", "of", and proof methods
    70 "rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
    65 "rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
    71 ("_") that stand for anonymous local variables.
    66 ("_") that stand for anonymous local variables.
       
    67 
       
    68 * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
       
    69 etc.) allow an optional context of local variables ('for' declaration):
       
    70 these variables become schematic in the instantiated theorem; this
       
    71 behaviour is analogous to 'for' in attributes "where" and "of".
       
    72 Configuration option rule_insts_schematic (default false) controls use
       
    73 of schematic variables outside the context. Minor INCOMPATIBILITY,
       
    74 declare rule_insts_schematic = true temporarily and update to use local
       
    75 variable declarations or dummy patterns instead.
    72 
    76 
    73 * Configuration option "rule_insts_schematic" determines whether proof
    77 * Configuration option "rule_insts_schematic" determines whether proof
    74 methods like "rule_tac" may refer to undeclared schematic variables
    78 methods like "rule_tac" may refer to undeclared schematic variables
    75 implicitly, instead of using proper 'for' declarations.  This historic
    79 implicitly, instead of using proper 'for' declarations.  This historic
    76 behaviour is still the default for some time.
    80 behaviour is still the default for some time.