- Explicitely applied predicate1I in a few proofs, because it is no longer
part of the claset
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set attribute, because it is no longer applied automatically
(* $Id$ *)
theory "locale" imports base begin
chapter {* Structured specifications *}
section {* Specification elements *}
text FIXME
section {* Type-inference *}
text FIXME
section {* Local theories *}
text {*
FIXME
\glossary{Local theory}{FIXME}
*}
end