equal
deleted
inserted
replaced
41 *** Pure *** |
41 *** Pure *** |
42 |
42 |
43 * Attributes "where" and "of" allow an optional context of local |
43 * Attributes "where" and "of" allow an optional context of local |
44 variables ('for' declaration): these variables become schematic in the |
44 variables ('for' declaration): these variables become schematic in the |
45 instantiated theorem. |
45 instantiated theorem. |
|
46 |
|
47 * Obsolete attribute "standard" has been discontinued (legacy since |
|
48 Isabelle2012). Potential INCOMPATIBILITY, use explicit 'for' context |
|
49 where instantiations with schematic variables are intended (for |
|
50 declaration commands like 'lemmas' or attributes like "of"). The |
|
51 following temporary definition may help to port old applications: |
|
52 |
|
53 attribute_setup standard = |
|
54 "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))" |
46 |
55 |
47 * More thorough check of proof context for goal statements and |
56 * More thorough check of proof context for goal statements and |
48 attributed fact expressions (concerning background theory, declared |
57 attributed fact expressions (concerning background theory, declared |
49 hyps). Potential INCOMPATIBILITY, tools need to observe standard |
58 hyps). Potential INCOMPATIBILITY, tools need to observe standard |
50 context discipline. See also Assumption.add_assumes and the more |
59 context discipline. See also Assumption.add_assumes and the more |