isabelle: src/HOL/Real/ROOT.ML@e7617b57a3e6 (annotated)

5078 7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	1	(* Title: HOL/Real/ROOT
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	2	ID: $Id$
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	5
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	6	Construction of the Reals using Dedekind Cuts, by Jacques Fleuriot
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	7	*)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	8
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	9	HOL_build_completed; (Make examples fail if HOL did)
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	10
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	11	writeln"Root file for HOL/Real";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	12
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	13	set proof_timing;
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	14	time_use_thy "RealAbs";
7b5ea59c0275 Installation of target HOL-Real paulson parents: diff changeset	15	time_use_thy "RComplete";

author	oheimb
	Mon, 21 Sep 1998 23:25:27 +0200
changeset 5526	e7617b57a3e6
parent 5078	7b5ea59c0275
child 5588	a3ab526bb891
permissions	-rw-r--r--