--- a/src/HOL/cladata.ML Thu Oct 12 12:15:59 2000 +0200
+++ b/src/HOL/cladata.ML Thu Oct 12 12:16:22 2000 +0200
@@ -50,7 +50,12 @@
end;
structure Classical = ClassicalFun(Classical_Data);
-structure BasicClassical: BASIC_CLASSICAL = Classical; open BasicClassical;
+
+structure BasicClassical: BASIC_CLASSICAL = Classical;
+open BasicClassical;
+
+bind_thm ("swap", inst "Pa" "?Q" swap);
+
structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);