TacticRecording « hol-light - proof-general - Emacs interface for proof assistants

Mode	Name	Size
-rw-r--r--	INSTRUCTIONS	1273	log plain
-rw-r--r--	LIMITATIONS	949	log plain
-rw-r--r--	biolayout.ml	1159	log plain
-rw-r--r--	dltree.ml	10119	log plain
-rw-r--r--	dltree.mli	1030	log plain
-rw-r--r--	ex.dot	359	log plain
-rw-r--r--	ex2.dot	180	log plain
-rw-r--r--	ex3.dot	390	log plain
-rw-r--r--	ex3.png	39644	log plain
-rw-r--r--	ex3b.dot	791	log plain
-rw-r--r--	examples1.ml	1159	log plain
-rw-r--r--	examples1_output.txt	1247	log plain
-rw-r--r--	examples2.ml	1471	log plain
-rw-r--r--	examples3.ml	9426	log plain
-rw-r--r--	examples3_LEMMA1.dot	339	log plain
-rw-r--r--	examples3_output.txt	1988	log plain
-rw-r--r--	examples4.ml	421	log plain
-rw-r--r--	examples5.ml	6877	log plain
-rw-r--r--	gvexport.ml	1924	log plain
-rw-r--r--	hiproofs.ml	12703	log plain
-rw-r--r--	lib.ml	1596	log plain
-rw-r--r--	main.ml	693	log plain
-rw-r--r--	mldata.ml	565	log plain
-rw-r--r--	mlexport.ml	6221	log plain
-rw-r--r--	printutils.ml	2079	log plain
-rw-r--r--	promote.ml	14010	log plain
-rw-r--r--	prooftree.ml	7037	log plain
-rw-r--r--	tacticrec.ml	12736	log plain
-rw-r--r--	wrappers.ml	13174	log plain
-rw-r--r--	xtactics.ml	17800	log plain
-rw-r--r--	xthm.ml	779	log plain