equal
deleted
inserted
replaced
82 |
82 |
83 * Antiquotation @{oracle_name} inlines a formally checked oracle name. |
83 * Antiquotation @{oracle_name} inlines a formally checked oracle name. |
84 |
84 |
85 |
85 |
86 *** System *** |
86 *** System *** |
|
87 |
|
88 * The command-line tool "isabelle imports" has been discontinued: strict |
|
89 checking of session directories enforces session-qualified theory names |
|
90 in applications -- users are responsible to specify session ROOT entries |
|
91 properly. |
87 |
92 |
88 * Theory export via Isabelle/Scala has been reworked. The former "fact" |
93 * Theory export via Isabelle/Scala has been reworked. The former "fact" |
89 name space is now split into individual "thm" items: names are |
94 name space is now split into individual "thm" items: names are |
90 potentially indexed, such as "foo" for singleton facts, or "bar(1)", |
95 potentially indexed, such as "foo" for singleton facts, or "bar(1)", |
91 "bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now |
96 "bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now |