doc-src/IsarRef/Thy/ROOT.ML
author berghofe
Wed, 07 May 2008 10:56:37 +0200
changeset 26795 a27607030a1c
parent 26782 19363c70b5c4
child 26840 ec46381f149d
permissions -rw-r--r--
- 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$ *)

use "../../antiquote_setup.ML";
use_thy "intro";
use_thy "syntax";
use_thy "pure";
use_thy "Generic";
use_thy "Quick_Reference";