Old_HOL: Integ/ROOT.ML@f04b33ce250f (annotated)

251 f04b33ce250f added calls of init_html and make_chart clasohm parents: 243 diff changeset	1	(* Title: Old_HOL/Integ/ROOT.ML
217 b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	2	ID: $Id$
b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	4	Copyright 1995 University of Cambridge
b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	5
b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	6	The Integers in HOL (ported from ZF by Riccardo Mattolini)
b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	7	*)
b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	8
b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	9	HOL_build_completed; (Cause examples to fail if HOL did)
b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	10
b6c0407f203e Installation of Integ (ported from ZF by Mattolini) lcp parents: diff changeset	11	loadpath := ["Integ"];
243 811481779743 Removed the "exit 1" calls, since now the lcp parents: 217 diff changeset	12	time_use_thy "Integ";
251 f04b33ce250f added calls of init_html and make_chart clasohm parents: 243 diff changeset	13
f04b33ce250f added calls of init_html and make_chart clasohm parents: 243 diff changeset	14	make_chart (); (make HTML chart)

author	clasohm
	Tue, 24 Oct 1995 14:59:17 +0100
changeset 251	f04b33ce250f
parent 243	811481779743
permissions	-rw-r--r--