| Tue, 26 Nov 1996 16:18:42 +0100 |
paulson |
Eta-expansion of a function definition, for value polymorphism
|
file |
diff |
annotate
|
| Fri, 01 Nov 1996 15:30:49 +0100 |
paulson |
asm_rewrite_goal_tac now calls SELECT_GOAL.
|
file |
diff |
annotate
|
| Mon, 30 Sep 1996 10:59:47 +0200 |
paulson |
prune_params_tac no longer rewrites main goal
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 11:10:46 +0200 |
paulson |
Generalized freeze to freeze_thaw in order to
|
file |
diff |
annotate
|
| Wed, 11 Sep 1996 18:00:53 +0200 |
nipkow |
renamed cterm_lift_inst_rule to term_lift_inst_rule and made it take
|
file |
diff |
annotate
|
| Mon, 09 Sep 1996 18:53:41 +0200 |
nipkow |
added cterm_lift_inst_rule
|
file |
diff |
annotate
|
| Thu, 05 Sep 1996 18:29:43 +0200 |
paulson |
Added thin_tac to signature; previous change was useless
|
file |
diff |
annotate
|
| Thu, 05 Sep 1996 10:29:52 +0200 |
paulson |
Declared thin_tac
|
file |
diff |
annotate
|
| Fri, 14 Jun 1996 12:27:11 +0200 |
paulson |
Added delete function for brls
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 12:34:18 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 14:16:13 +0100 |
clasohm |
inserted tabs again
|
file |
diff |
annotate
|
| Mon, 29 Jan 1996 13:56:41 +0100 |
clasohm |
removed tabs
|
file |
diff |
annotate
|
| Fri, 28 Jul 1995 17:24:53 +0200 |
nipkow |
added rotate_tac.
|
file |
diff |
annotate
|
| Fri, 28 Apr 1995 11:52:43 +0200 |
lcp |
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
|
file |
diff |
annotate
|
| Tue, 14 Mar 1995 10:40:04 +0100 |
nipkow |
Removed an old bug which made some simultaneous instantiations fail if they
|
file |
diff |
annotate
|
| Mon, 13 Mar 1995 09:38:10 +0100 |
nipkow |
Changed treatment of during type inference internally generated type
|
file |
diff |
annotate
|
| Sat, 11 Mar 1995 11:58:21 +0100 |
lcp |
Put freeze into the signature TACTIC for export
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 11:48:05 +0100 |
clasohm |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
file |
diff |
annotate
|
| Thu, 08 Dec 1994 11:26:25 +0100 |
lcp |
res_inst_tac: added comments
|
file |
diff |
annotate
|
| Mon, 31 Oct 1994 18:01:02 +0100 |
lcp |
Pure/tactic/build_netpair: now takes two arguments
|
file |
diff |
annotate
|
| Fri, 24 Jun 1994 10:45:02 +0200 |
lcp |
Pure/tactic/subgoals_tac: new (moved from ZF/Order.ML)
|
file |
diff |
annotate
|
| Wed, 16 Feb 1994 13:56:20 +0100 |
lcp |
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
|
file |
diff |
annotate
|
| Tue, 18 Jan 1994 15:57:40 +0100 |
lcp |
Many other files modified as follows:
|
file |
diff |
annotate
|
| Wed, 05 Jan 1994 19:33:56 +0100 |
nipkow |
added new parameter to the simplification tactics which indicates if
|
file |
diff |
annotate
|
| Fri, 10 Dec 1993 10:36:39 +0100 |
lcp |
Pure/tactic/compose_inst_tac: when catching exception THM, prints the
|
file |
diff |
annotate
|
| Fri, 22 Oct 1993 11:25:15 +0100 |
lcp |
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|