equal
deleted
inserted
replaced
585 lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" . |
585 lemma thin_refl: "!!X. [|p:x=x; PROP W|] ==> PROP W" . |
586 |
586 |
587 use "hypsubst.ML" |
587 use "hypsubst.ML" |
588 |
588 |
589 ML {* |
589 ML {* |
590 |
590 structure Hypsubst = Hypsubst |
591 (*** Applying HypsubstFun to generate hyp_subst_tac ***) |
591 ( |
592 |
|
593 structure Hypsubst_Data = |
|
594 struct |
|
595 (*Take apart an equality judgement; otherwise raise Match!*) |
592 (*Take apart an equality judgement; otherwise raise Match!*) |
596 fun dest_eq (Const (@{const_name Proof}, _) $ |
593 fun dest_eq (Const (@{const_name Proof}, _) $ |
597 (Const (@{const_name eq}, _) $ t $ u) $ _) = (t, u); |
594 (Const (@{const_name eq}, _) $ t $ u) $ _) = (t, u); |
598 |
595 |
599 val imp_intr = @{thm impI} |
596 val imp_intr = @{thm impI} |
603 |
600 |
604 val rev_mp = @{thm rev_mp} |
601 val rev_mp = @{thm rev_mp} |
605 val subst = @{thm subst} |
602 val subst = @{thm subst} |
606 val sym = @{thm sym} |
603 val sym = @{thm sym} |
607 val thin_refl = @{thm thin_refl} |
604 val thin_refl = @{thm thin_refl} |
608 end; |
605 ); |
609 |
|
610 structure Hypsubst = HypsubstFun(Hypsubst_Data); |
|
611 open Hypsubst; |
606 open Hypsubst; |
612 *} |
607 *} |
613 |
608 |
614 use "intprover.ML" |
609 use "intprover.ML" |
615 |
610 |