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

author | wenzelm |

Fri, 21 Oct 2005 18:14:44 +0200 | |

changeset 17964 | 6842ca6ecb87 |

parent 17963 | 5574f676092c |

child 17965 | fa380d7d4931 |

renamed triv_goal to goalI, rev_triv_goal to goalD;
removed mk_triv_goal (cf. Goal.init);

src/Pure/drule.ML | file | annotate | diff | comparison | revisions |

--- a/src/Pure/drule.ML Fri Oct 21 18:14:43 2005 +0200 +++ b/src/Pure/drule.ML Fri Oct 21 18:14:44 2005 +0200 @@ -126,11 +126,10 @@ val norm_hhf_eq: thm val is_norm_hhf: term -> bool val norm_hhf: theory -> term -> term - val triv_goal: thm - val rev_triv_goal: thm + val goalI: thm + val goalD: thm val implies_intr_goals: cterm list -> thm -> thm val freeze_all: thm -> thm - val mk_triv_goal: cterm -> thm val tvars_of_terms: term list -> (indexname * sort) list val vars_of_terms: term list -> (indexname * typ) list val tvars_of: thm -> (indexname * sort) list @@ -929,21 +928,20 @@ val G = Logic.mk_goal A; val (G_def, _) = freeze_thaw ProtoPure.Goal_def; in - val triv_goal = store_thm "triv_goal" (kind_rule internalK (standard + val goalI = store_thm "goalI" (kind_rule internalK (standard (Thm.equal_elim (Thm.symmetric G_def) (Thm.assume (cert A))))); - val rev_triv_goal = store_thm "rev_triv_goal" (kind_rule internalK (standard + val goalD = store_thm "goalD" (kind_rule internalK (standard (Thm.equal_elim G_def (Thm.assume (cert G))))); end; val mk_cgoal = Thm.capply (Thm.cterm_of ProtoPure.thy Logic.goal_const); -fun assume_goal ct = Thm.assume (mk_cgoal ct) RS rev_triv_goal; +fun assume_goal ct = Thm.assume (mk_cgoal ct) RS goalD; fun implies_intr_goals cprops thm = implies_elim_list (implies_intr_list cprops thm) (map assume_goal cprops) |> implies_intr_list (map mk_cgoal cprops); - (** variations on instantiate **) (*shorthand for instantiating just one variable in the current theory*) @@ -1091,12 +1089,6 @@ val freeze_all = freeze_all_Vars o freeze_all_TVars; -(* mk_triv_goal *) - -(*make an initial proof state, "PROP A ==> (PROP A)" *) -fun mk_triv_goal ct = instantiate' [] [SOME ct] triv_goal; - - (** meta-level conjunction **)