moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
use_thys [
"Eq",
"Integration",
"Isar",
"Local_Theory",
"Logic",
"ML",
"Prelim",
"Proof",
"Syntax",
"Tactic"
];