--- a/src/FOL/ROOT.ML Wed Aug 25 20:42:01 1999 +0200
+++ b/src/FOL/ROOT.ML Wed Aug 25 20:45:19 1999 +0200
@@ -1,10 +1,9 @@
-(* Title: FOL/ROOT
+(* Title: FOL/ROOT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-Adds First-Order Logic to a database containing pure Isabelle.
-Should be executed in the subdirectory FOL.
+First-Order Logic.
*)
val banner = "First-Order Logic with Natural Deduction";
@@ -23,39 +22,6 @@
use "~~/src/Provers/quantifier1.ML";
use_thy "IFOL";
-use "fologic.ML";
-
-(** Applying HypsubstFun to generate hyp_subst_tac **)
-structure Hypsubst_Data =
- struct
- structure Simplifier = Simplifier
- (*These destructors Match!*)
- fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T)
- val dest_Trueprop = FOLogic.dest_Trueprop
- val dest_imp = FOLogic.dest_imp
- val eq_reflection = eq_reflection
- val imp_intr = impI
- val rev_mp = rev_mp
- val subst = subst
- val sym = sym
- val thin_refl = prove_goal IFOL.thy
- "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
- end;
-
-structure Hypsubst = HypsubstFun(Hypsubst_Data);
-open Hypsubst;
-
-
-use "intprover.ML";
-
use_thy "FOL";
-use "cladata.ML";
-use "simpdata.ML";
-
-qed_goal "ex1_functional" FOL.thy
- "!!a b c. [| EX! z. P(a,z); P(a,b); P(a,c) |] ==> b = c"
- (fn _ => [ (Blast_tac 1) ]);
-
-
print_depth 8;