doc-src/IsarImplementation/Thy/ROOT.ML
author huffman
Thu, 08 Jan 2009 09:12:29 -0800
changeset 29405 98ab21b14f09
parent 20472 e993073eda4c
child 29755 d66b34e46bdf
child 30240 5b25fee0362c
permissions -rw-r--r--
add class ring_div; generalize mod/diff/minus proofs for class ring_div


(* $Id$ *)

use_thy "prelim";
use_thy "logic";
use_thy "tactic";
use_thy "proof";
use_thy "isar";
use_thy "locale";
use_thy "integration";
use_thy "ML";