doc-src/TutorialI/Rules/ROOT.ML
author blanchet
Mon, 19 Apr 2010 18:14:45 +0200
changeset 36230 43d10a494c91
parent 16546 77e7fd18b785
child 42637 381fdcab0f36
permissions -rw-r--r--
added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent

(* ID:         $Id$ *)
use_thy "Basic";
use_thy "Blast";
use_thy "Force";
use_thy "Forward";
use_thy "Tacticals";

use_thy "find2";