isabelle: src/HOL/MiniML/ROOT.ML@f999804f11ea (annotated)

1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	1	(* Title: HOL/MiniML/ROOT.ML
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	2	ID: $Id$
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	3	Author: Tobias Nipkow
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	4	Copyright 1995 TUM
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	5
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	6	Type inference for let-free MiniML
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	7	*)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	8
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	9	HOL_build_completed; (Make examples fail if HOL did)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	10
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	11	writeln"Root file for HOL/MiniML";
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	12	Unify.trace_bound := 20;
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	13
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	14	time_use_thy "I";

author	nipkow
	Thu, 22 Feb 1996 18:35:16 +0100
changeset 1519	f999804f11ea
parent 1351	4a960c012383
child 1925	1150f128c7fe
permissions	-rw-r--r--