equal
deleted
inserted
replaced
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 |