Index of /ftp/hvg/hol88/contrib/SECD

	Name	Last modified	Size	Description
	Parent Directory		-
	CU_proofs.ml	1993-01-07 11:18	30K
	CU_wordn_proofs.ml	1993-01-07 11:18	2.7K
	DP_proofs.ml	1993-01-07 11:18	7.8K
	Inc9_proofs.ml	1993-01-07 11:18	6.7K
	Makefile	1993-01-07 11:18	16K
	READ-ME	1995-05-25 12:39	6.2K
	SECD_proofs.ml	1993-01-07 11:18	14K
	STATS/	1992-12-04 12:51	-
	SYS_proofs.ml	1993-01-07 11:18	32K
	TACTICS/	1992-12-04 12:51	-
	abstract_mem_type.ml	1993-01-07 11:18	24K
	buses/	1992-12-04 12:51	-
	constraints.ml	1993-01-07 11:18	43K
	correctness.ml	1993-01-07 11:18	14K
	correctness_ADD.ml	1993-01-07 11:18	9.5K
	correctness_AP.ml	1993-01-07 11:18	11K
	correctness_ATOM.ml	1993-01-07 11:18	8.2K
	correctness_CAR.ml	1993-01-07 11:18	7.9K
	correctness_CDR.ml	1993-01-07 11:18	7.9K
	correctness_CONS.ml	1993-01-07 11:18	8.8K
	correctness_DUM.ml	1993-01-07 11:18	7.4K
	correctness_EQ.ml	1993-01-07 11:18	9.2K
	correctness_JOIN.ml	1993-01-07 11:18	7.1K
	correctness_LD.ml	1993-01-07 11:18	13K
	correctness_LDC.ml	1993-01-07 11:18	8.4K
	correctness_LDF.ml	1993-01-07 11:18	8.2K
	correctness_LEQ.ml	1993-01-07 11:18	9.2K
	correctness_RAP.ml	1993-01-07 11:18	19K
	correctness_RTN.ml	1993-01-07 11:18	9.1K
	correctness_SEL.ml	1993-01-07 11:18	17K
	correctness_STOP.ml	1993-01-07 11:18	7.9K
	correctness_SUB.ml	1993-01-07 11:18	9.5K
	correctness_init.ml	1993-01-07 11:18	13K
	correctness_misc.ml	1993-01-07 11:18	60K
	cu_types.ml	1993-01-07 11:18	5.0K
	dp_types.ml	1993-01-07 11:18	18K
	hol-init.ml	1993-01-07 11:18	1.9K
	interface.ml	1993-01-07 11:18	10K
	intermediate	1993-01-07 11:18	7.1K
	io.ml	1993-01-07 11:18	4.0K
	liveness.ml	1993-01-07 11:18	8.2K
	loop_proofs.ml	1993-01-07 11:18	22K
	mem_abs.ml	1993-01-07 11:18	31K
	microcode.ml	1993-01-07 11:18	11K
	modulo_ops.ml	1993-01-07 11:18	22K
	mu-prog_ADD.ml	1993-01-07 11:18	351
	mu-prog_AP.ml	1993-01-07 11:18	6.2K
	mu-prog_ATOM.ml	1993-01-07 11:18	358
	mu-prog_CAR.ml	1993-01-07 11:18	351
	mu-prog_CDR.ml	1993-01-07 11:18	351
	mu-prog_CONS.ml	1993-01-07 11:18	358
	mu-prog_DUM.ml	1993-01-07 11:18	351
	mu-prog_EQ.ml	1993-01-07 11:18	344
	mu-prog_JOIN.ml	1993-01-07 11:18	358
	mu-prog_LD.ml	1993-01-07 11:18	8.9K
	mu-prog_LD1.ml	1993-01-07 11:18	6.9K
	mu-prog_LD2.ml	1993-01-07 11:18	21K
	mu-prog_LDC.ml	1993-01-07 11:18	351
	mu-prog_LDF.ml	1993-01-07 11:18	352
	mu-prog_LEQ.ml	1993-01-07 11:18	338
	mu-prog_RAP.ml	1993-01-07 11:18	6.1K
	mu-prog_RTN.ml	1993-01-07 11:18	351
	mu-prog_SEL.ml	1993-01-07 11:18	351
	mu-prog_STOP.ml	1993-01-07 11:18	359
	mu-prog_SUB.ml	1993-01-07 11:18	350
	mu-prog_init_proofs.ml	1993-01-07 11:18	5.9K
	mu-prog_level.ml	1993-01-07 11:18	6.6K
	mu-prog_proof0.ml	1993-01-07 11:18	5.1K
	mu-prog_proof_fcn.ml	1993-01-07 11:18	21K
	mu-prog_sr_proofs.ml	1993-01-07 11:18	16K
	phase_lemmas1.ml	1993-01-07 11:18	1.1K
	phase_lemmas2.ml	1993-01-07 11:18	1.0K
	phase_lemmas3.ml	1993-01-07 11:18	1.1K
	phase_lemmas4.ml	1993-01-07 11:18	1.1K
	phase_lemmas5.ml	1993-01-07 11:18	1.1K
	phase_lemmas6.ml	1993-01-07 11:18	5.8K
	phase_lemmas7.ml	1993-01-07 11:18	1.1K
	phase_proof_fcn.ml	1993-01-07 11:18	15K
	phase_template.ml	1993-01-07 11:18	5.7K
	rt_CU.ml	1993-01-07 11:18	14K
	rt_DP.ml	1993-01-07 11:18	16K
	rt_PADS.ml	1993-01-07 11:18	6.7K
	rt_SECD.ml	1993-01-07 11:18	6.8K
	rt_SYS.ml	1993-01-07 11:18	5.0K
	simplify.ml	1993-01-07 11:18	20K
	top_SECD.ml	1993-01-07 11:18	30K
	val_defs.ml	1993-01-07 11:18	1.8K
	val_theorems.ml	1993-01-07 11:18	31K
	when.ml	1993-01-07 11:18	15K
	wordn/	1992-12-04 12:51	-