changeset 4096 | 8cdf672a83e8 |
parent 4024 | 3c056eab237c |
child 4179 | cc4b6791d5dc |
--- a/src/FOL/ROOT.ML Mon Nov 03 12:28:14 1997 +0100 +++ b/src/FOL/ROOT.ML Mon Nov 03 12:28:45 1997 +0100 @@ -43,6 +43,9 @@ 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 _ => [ (deepen_tac FOL_cs 0 1) ]);