equal
deleted
inserted
replaced
232 name space is now split into individual "thm" items: names are |
232 name space is now split into individual "thm" items: names are |
233 potentially indexed, such as "foo" for singleton facts, or "bar(1)", |
233 potentially indexed, such as "foo" for singleton facts, or "bar(1)", |
234 "bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now |
234 "bar(2)", "bar(3)" for multi-facts. Theorem dependencies are now |
235 exported as well: this spans an overall dependency graph of internal |
235 exported as well: this spans an overall dependency graph of internal |
236 inferences; it might help to reconstruct the formal structure of theory |
236 inferences; it might help to reconstruct the formal structure of theory |
237 libraries. See also the module Export_Theory in Isabelle/Scala. |
237 libraries. See also the module isabelle.Export_Theory in Isabelle/Scala. |
238 |
238 |
239 * Theory export of structured specifications, based on internal |
239 * Theory export of structured specifications, based on internal |
240 declarations of Spec_Rules by packages like 'definition', 'inductive', |
240 declarations of Spec_Rules by packages like 'definition', 'inductive', |
241 'primrec', 'function'. |
241 'primrec', 'function'. |
242 |
242 |