summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Fri, 31 Aug 2001 16:29:18 +0200 | |

changeset 11534 | 0494d0347f18 |

parent 11533 | 0c0d2332e8f0 |

child 11535 | 7f4c5cdea239 |

Proof of True_implies_equals is stored with "open" derivation to
facilitate simplification of proof terms.

--- a/src/HOL/simpdata.ML Fri Aug 31 16:28:26 2001 +0200 +++ b/src/HOL/simpdata.ML Fri Aug 31 16:29:18 2001 +0200 @@ -105,11 +105,11 @@ (* Elimination of True from asumptions: *) -val True_implies_equals = prove_goal (the_context ()) - "(True ==> PROP P) == PROP P" -(fn _ => [rtac equal_intr_rule 1, atac 2, - METAHYPS (fn prems => resolve_tac prems 1) 1, - rtac TrueI 1]); +local fun rd s = read_cterm (sign_of (the_context())) (s, propT); +in val True_implies_equals = standard' (equal_intr + (implies_intr_hyps (implies_elim (assume (rd "True ==> PROP P")) TrueI)) + (implies_intr_hyps (implies_intr (rd "True") (assume (rd "PROP P"))))); +end; fun prove nm thm = qed_goal nm (the_context ()) thm (fn _ => [(Blast_tac 1)]);