doc-src/IsarRef/Thy/ROOT.ML
author wenzelm
Tue, 10 Jun 2008 19:15:20 +0200
changeset 27127 cd6617d57a16
parent 27048 0e86aab627f3
child 28751 aad88e7344f0
permissions -rw-r--r--
added HOL/Tools/induct_tacs.ML;


(* $Id$ *)

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

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