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

2031 03a843f0f447 Ran expandshort paulson parents: 1925 diff changeset	1	(* Title: HOL/MiniML/ROOT.ML
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	2	ID: $Id$
2525 477c05586286 The new version of MiniML including "let". nipkow parents: 2031 diff changeset	3	Author: Wolfgang Naraschewski and Tobias Nipkow
1300 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
2525 477c05586286 The new version of MiniML including "let". nipkow parents: 2031 diff changeset	6	Type inference for MiniML
1300 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
2031 03a843f0f447 Ran expandshort paulson parents: 1925 diff changeset	9	HOL_build_completed; (Make examples fail if HOL did)
1300 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
2525 477c05586286 The new version of MiniML including "let". nipkow parents: 2031 diff changeset	13	time_use_thy "W";