src/HOL/cladata.ML
changeset 7357 d0e16da40ea2
parent 7153 820c8c8573d9
child 8099 6a087be9f6d9
     1.1 --- a/src/HOL/cladata.ML	Wed Aug 25 20:46:40 1999 +0200
     1.2 +++ b/src/HOL/cladata.ML	Wed Aug 25 20:49:02 1999 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4    val rev_mp = rev_mp
     1.5    val subst = subst
     1.6    val sym = sym
     1.7 -  val thin_refl = prove_goal HOL.thy 
     1.8 +  val thin_refl = prove_goal (the_context ())
     1.9  		  "!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
    1.10    end;
    1.11  
    1.12 @@ -40,7 +40,8 @@
    1.13    end;
    1.14  
    1.15  structure Classical = ClassicalFun(Classical_Data);
    1.16 -open Classical;
    1.17 +structure BasicClassical: BASIC_CLASSICAL = Classical;
    1.18 +open BasicClassical;
    1.19  
    1.20  (*Propositional rules*)
    1.21  val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI]
    1.22 @@ -50,38 +51,4 @@
    1.23  val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, select_equality] 
    1.24                       addSEs [exE] addEs [allE];
    1.25  
    1.26 -claset_ref() := HOL_cs;
    1.27 -
    1.28 -(*Better then ex1E for classical reasoner: needs no quantifier duplication!*)
    1.29 -val major::prems = goal thy
    1.30 -    "[| ?! x. P(x);                                              \
    1.31 -\       !!x. [| P(x);  ALL y y'. P(y) & P(y') --> y=y' |] ==> R  \
    1.32 -\    |] ==> R";
    1.33 -by (rtac (major RS ex1E) 1);
    1.34 -by (REPEAT (ares_tac (allI::prems) 1));
    1.35 -by (etac (dup_elim allE) 1);
    1.36 -by (Fast_tac 1);
    1.37 -qed "alt_ex1E";
    1.38 -
    1.39 -AddSEs [alt_ex1E];
    1.40 -
    1.41 -(*** Applying BlastFun to create Blast_tac ***)
    1.42 -structure Blast_Data = 
    1.43 -  struct
    1.44 -  type claset	= Classical.claset
    1.45 -  val notE	= notE
    1.46 -  val ccontr	= ccontr
    1.47 -  val contr_tac = Classical.contr_tac
    1.48 -  val dup_intr	= Classical.dup_intr
    1.49 -  val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    1.50 -  val claset	= Classical.claset
    1.51 -  val rep_cs    = Classical.rep_cs
    1.52 -  val cla_modifiers = Classical.cla_modifiers;
    1.53 -  val cla_meth' = Classical.cla_meth'
    1.54 -  end;
    1.55 -
    1.56 -structure Blast = BlastFun(Blast_Data);
    1.57 -Blast.overloaded ("op =", domain_type);	(*overloading of equality as iff*)
    1.58 -
    1.59 -val Blast_tac = Blast.Blast_tac
    1.60 -and blast_tac = Blast.blast_tac;
    1.61 +val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)];