isabelle: src/HOL/MiniML/ROOT.ML@1150f128c7fe (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
1925 1150f128c7fe Some tidying. This brittle proof depends upon paulson parents: 1351 diff changeset	14	AddSEs [less_SucE];
1150f128c7fe Some tidying. This brittle proof depends upon paulson parents: 1351 diff changeset	15
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	16	time_use_thy "I";

author	paulson
	Tue, 20 Aug 1996 12:32:16 +0200
changeset 1925	1150f128c7fe
parent 1351	4a960c012383
child 2031	03a843f0f447
permissions	-rw-r--r--