src/HOL/cladata.ML
changeset 10197 4ea3ee8de019
parent 9969 4753185f1dd2
child 10231 178a272bceeb
     1.1 --- a/src/HOL/cladata.ML	Thu Oct 12 12:15:59 2000 +0200
     1.2 +++ b/src/HOL/cladata.ML	Thu Oct 12 12:16:22 2000 +0200
     1.3 @@ -50,7 +50,12 @@
     1.4    end;
     1.5  
     1.6  structure Classical = ClassicalFun(Classical_Data);
     1.7 -structure BasicClassical: BASIC_CLASSICAL = Classical; open BasicClassical;
     1.8 +
     1.9 +structure BasicClassical: BASIC_CLASSICAL = Classical; 
    1.10 +open BasicClassical;
    1.11 +
    1.12 +bind_thm ("swap", inst "Pa" "?Q" swap);
    1.13 +
    1.14  structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
    1.15    that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);
    1.16