https://github.com/theoremprover-museum/CLIN
Raw File
Tip revision: e7082fbde3634286f458d64846699ae488fe18f3 authored by Michael Kohlhase on 22 December 2016, 09:28:55 UTC
initial commit, thanks to David Plaisted
Tip revision: e7082fb
files_changed

	Compared with /rho/plaisted/lee/clin/ where the original prover is.

	auxiliary: floor functions.
	clausify:  no change
	command:   assign/2 to assign_cmd/2.
	define:	   new
	exprules:  no change
	fls:	   cputime, line 70, bagof1 the first argument X changed to Z.
	hyper:	   cputime, hl_literals call at 286,  proc_C at 792
	instdel:   cputime, 52 add erase(Ref1)
	interp:	   cputime, interp_1 added interp_1_define to take care of
		   'define' stuff. Correct argument bug (one missing) in 
		   ubfsupp_o_1/7.
	library:   appended removed for Quintus.
	main:	   floor, cputime, call(X) at line 286, assign_cmd at 432.
	pc:	   cputime, reduce_set_1/10 bug corrected.
	prover:	   just file names, actually directory.
	replace:   cputime
	simplify:  cputime, change binary_max_ind/4 at 408
	skolem:    new
	spc:	   cputime
	try:	   cputime, floor at 485
	xvisor:	   change assign/2 to assign_cmd/2, all of them.
back to top