doc-src/IsarRef/Thy/ROOT.ML

refined notion of derivation, consiting of promises and proof_body;
removed oracle_of (would require detailed check wrt. promises);
proof_of returns proof_body;

(* $Id$ *)

set ThyOutput.source;
use "../../antiquote_setup.ML";

use_thy "Introduction";
use_thy "Outer_Syntax";
use_thy "Document_Preparation";
use_thy "Spec";
use_thy "Proof";
use_thy "Inner_Syntax";
use_thy "Misc";
use_thy "Generic";
use_thy "HOL_Specific";
use_thy "Quick_Reference";
use_thy "ML_Tactic";