# HG changeset patch
# User paulson
# Date 971345782 -7200
# Node ID 4ea3ee8de0198dbabb56f8f7d06bb0a541c53167
# Parent  4d1af711cf7ba291c31b044af5b315b570565e4d
renamed ?Pa to ?Q in swap

diff -r 4d1af711cf7b -r 4ea3ee8de019 src/HOL/cladata.ML
--- 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]);