src/HOL/cladata.ML
changeset 4206 688050e83d89
parent 4205 96632970d203
child 4223 f60e3d2c81d3
equal deleted inserted replaced
4205:96632970d203 4206:688050e83d89
    24   end;
    24   end;
    25 
    25 
    26 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    26 structure Hypsubst = HypsubstFun(Hypsubst_Data);
    27 open Hypsubst;
    27 open Hypsubst;
    28 
    28 
    29 val thin_refl = prove_goal HOL.thy 
       
    30 	"!!X. [|x=x; PROP W|] ==> PROP W" (K [atac 1]);
       
    31 
       
    32 (*** Applying ClassicalFun to create a classical prover ***)
    29 (*** Applying ClassicalFun to create a classical prover ***)
    33 structure Classical_Data = 
    30 structure Classical_Data = 
    34   struct
    31   struct
    35   val sizef     = size_of_thm
    32   val sizef     = size_of_thm
    36   val mp        = mp
    33   val mp        = mp
    37   val not_elim  = notE
    34   val not_elim  = notE
    38   val classical = classical
    35   val classical = classical
    39   val thin_refl = thin_refl
    36   val hyp_subst_tacs=[hyp_subst_tac]
    40   val hyp_subst_tacs= [REPEAT_DETERM o ematch_tac [thin_refl] THEN' hyp_subst_tac]
       
    41   end;
    37   end;
    42 
    38 
    43 structure Classical = ClassicalFun(Classical_Data);
    39 structure Classical = ClassicalFun(Classical_Data);
    44 open Classical;
    40 open Classical;
    45 
    41