src/HOL/cladata.ML
changeset 10231 178a272bceeb
parent 10197 4ea3ee8de019
child 10383 a092ae7bb2a6
     1.1 --- a/src/HOL/cladata.ML	Tue Oct 17 10:20:43 2000 +0200
     1.2 +++ b/src/HOL/cladata.ML	Tue Oct 17 10:21:12 2000 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  structure BasicClassical: BASIC_CLASSICAL = Classical; 
     1.5  open BasicClassical;
     1.6  
     1.7 -bind_thm ("swap", inst "Pa" "?Q" swap);
     1.8 +bind_thm ("contrapos_np", inst "Pa" "?Q" swap);
     1.9  
    1.10  structure Obtain = ObtainFun(val atomic_thesis = HOLogic.atomic_Trueprop and
    1.11    that_atts = [Simplifier.simp_add_local, Classical.haz_intro_local]);