Mon, 15 May 2000 17:32:39 +0200 alist_rec and assoc are now defined using primrec and thus no longer
berghofe [Mon, 15 May 2000 17:32:39 +0200] rev 8874
alist_rec and assoc are now defined using primrec and thus no longer refer to the recursion combinator list_rec, which should be considered internal.
Mon, 15 May 2000 17:30:19 +0200 Removed unnecessary primrec equations of hd and last involving arbitrary.
berghofe [Mon, 15 May 2000 17:30:19 +0200] rev 8873
Removed unnecessary primrec equations of hd and last involving arbitrary.
Mon, 15 May 2000 10:34:51 +0200 collected three proofs into rename_client_map_tac
paulson [Mon, 15 May 2000 10:34:51 +0200] rev 8872
collected three proofs into rename_client_map_tac
(0) -3000 -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip