lcp [Fri, 14 Apr 1995 11:26:22 +0200] rev 1058
Deleted comment
lcp [Fri, 14 Apr 1995 11:25:23 +0200] rev 1057
Renamed diff_sing_lepoll to Diff_sing_lepoll.
lcp [Fri, 14 Apr 1995 11:24:51 +0200] rev 1056
Renamed domain_diff_subset, range_diff_subset,
field_diff_subset, converse_diff to domain_Diff_subset, range_Diff_subset,
field_Diff_subset, converse_Diff for consistency. (Thanks to KG)
lcp [Fri, 14 Apr 1995 11:24:10 +0200] rev 1055
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
to Diff_sing_lepoll, lepoll_Diff_sing and Diff_sing_eqpoll for consistency.
Strengthened lepoll_Diff_sing. (Thanks to KG)
lcp [Fri, 14 Apr 1995 11:22:30 +0200] rev 1054
Updated CADE reference
lcp [Fri, 14 Apr 1995 11:20:53 +0200] rev 1053
Removes (obsolete) target if already present.
nipkow [Thu, 13 Apr 1995 17:05:41 +0200] rev 1052
Olafs new version.
nipkow [Thu, 13 Apr 1995 16:57:18 +0200] rev 1051
Directory example is now called NTP
nipkow [Thu, 13 Apr 1995 16:55:14 +0200] rev 1050
ABP: Alternating bit protocol example
nipkow [Thu, 13 Apr 1995 16:53:15 +0200] rev 1049
New ROOT file.
lcp [Thu, 13 Apr 1995 15:38:07 +0200] rev 1048
New example by Ole Rasmussen
lcp [Thu, 13 Apr 1995 15:13:27 +0200] rev 1047
Simplified some proofs and made them work for new hyp_subst_tac.
lcp [Thu, 13 Apr 1995 15:08:39 +0200] rev 1046
expandshort
lcp [Thu, 13 Apr 1995 15:06:25 +0200] rev 1045
Deleted some useless things and made proofs of
refl_comp_subset and comp_equivI more like the versions in ZF/EquivClass.ML
lcp [Thu, 13 Apr 1995 15:03:07 +0200] rev 1044
Simplified using pattern replacements.