equal
deleted
inserted
replaced
916 val imp_intr = @{thm impI} |
916 val imp_intr = @{thm impI} |
917 val rev_mp = @{thm rev_mp} |
917 val rev_mp = @{thm rev_mp} |
918 val subst = @{thm subst} |
918 val subst = @{thm subst} |
919 val sym = @{thm sym} |
919 val sym = @{thm sym} |
920 val thin_refl = @{thm thin_refl}; |
920 val thin_refl = @{thm thin_refl}; |
|
921 val prop_subst = @{lemma "PROP P t ==> PROP prop (x = t ==> PROP P x)" |
|
922 by (unfold prop_def) (drule eq_reflection, unfold)} |
921 end); |
923 end); |
922 open Hypsubst; |
924 open Hypsubst; |
923 |
925 |
924 structure Classical = ClassicalFun( |
926 structure Classical = ClassicalFun( |
925 struct |
927 struct |