isabelle: File revisions

src/Pure/tactic.ML

1996-11-01	paulson	1996-11-01	asm_rewrite_goal_tac now calls SELECT_GOAL. Replaced min by Int.min	file \| diff \| annotate
1996-09-30	paulson	1996-09-30	prune_params_tac no longer rewrites main goal	file \| diff \| annotate
1996-09-26	paulson	1996-09-26	Generalized freeze to freeze_thaw in order to implement defer_tac	file \| diff \| annotate
1996-09-11	nipkow	1996-09-11	renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take uncertified things, because they need to be recertified anyway.	file \| diff \| annotate
1996-09-09	nipkow	1996-09-09	added cterm_lift_inst_rule	file \| diff \| annotate
1996-09-05	paulson	1996-09-05	Added thin_tac to signature; previous change was useless	file \| diff \| annotate
1996-09-05	paulson	1996-09-05	Declared thin_tac	file \| diff \| annotate
1996-06-14	paulson	1996-06-14	Added delete function for brls	file \| diff \| annotate
1996-02-16	paulson	1996-02-16	Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.	file \| diff \| annotate
1996-01-29	clasohm	1996-01-29	inserted tabs again	file \| diff \| annotate
1996-01-29	clasohm	1996-01-29	removed tabs	file \| diff \| annotate
1995-07-28	nipkow	1995-07-28	added rotate_tac.	file \| diff \| annotate
1995-04-28	lcp	1995-04-28	Renamed insert_kbrl to insert_tagged_brl and exported it. Now subgoals_of_brl calls nprems_of, which is faster than length o prems_of.	file \| diff \| annotate
1995-03-14	nipkow	1995-03-14	Removed an old bug which made some simultaneous instantiations fail if they were given in the "wrong" order. Rewrote sign/infer_types. Fixed some comments.	file \| diff \| annotate
1995-03-13	nipkow	1995-03-13	Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.	file \| diff \| annotate
1995-03-11	lcp	1995-03-11	Put freeze into the signature TACTIC for export	file \| diff \| annotate
1995-03-03	clasohm	1995-03-03	added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)	file \| diff \| annotate
1994-12-08	lcp	1994-12-08	res_inst_tac: added comments	file \| diff \| annotate
1994-10-31	lcp	1994-10-31	Pure/tactic/build_netpair: now takes two arguments	file \| diff \| annotate
1994-06-24	lcp	1994-06-24	Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)	file \| diff \| annotate
1994-02-16	lcp	1994-02-16	tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead instantiate changes the indices of V and W. tactic/cut_inst_tac: new	file \| diff \| annotate
1994-01-18	lcp	1994-01-18	Many other files modified as follows: s\|Sign.cterm\|cterm\|g s\|Sign.ctyp\|ctyp\|g s\|Sign.rep_cterm\|rep_cterm\|g s\|Sign.rep_ctyp\|rep_ctyp\|g s\|Sign.pprint_cterm\|pprint_cterm\|g s\|Sign.pprint_ctyp\|pprint_ctyp\|g s\|Sign.string_of_cterm\|string_of_cterm\|g s\|Sign.string_of_ctyp\|string_of_ctyp\|g s\|Sign.term_of\|term_of\|g s\|Sign.typ_of\|typ_of\|g s\|Sign.read_cterm\|read_cterm\|g s\|Sign.read_insts\|read_insts\|g s\|Sign.cfun\|cterm_fun\|g	file \| diff \| annotate
1994-01-05	nipkow	1994-01-05	added new parameter to the simplification tactics which indicates if assumptions are to be simplified and/or to be used when simplifying the conclusion. This gets rid of METAHYPS and speeds up simplification of goals with big assumptions.	file \| diff \| annotate
1993-12-10	lcp	1993-12-10	Pure/tactic/compose_inst_tac: when catching exception THM, prints the message before failing!! This reports the reason for failure in cases like by (res_inst_tac [("P", "?Q(a)")] mp 1); in which ?Q appears in mp with a different type.	file \| diff \| annotate
1993-10-22	lcp	1993-10-22	tactic/fold_tac,fold_goals_tac: now handle critical pairs on the right sides of the defs	file \| diff \| annotate
1993-09-16	clasohm	1993-09-16	Initial revision	file \| diff \| annotate

isabelle

RSS Atom