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. 