isabelle: src/HOL/MiniML/ROOT.ML@902ec83c1ca9 (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
2525 477c05586286 The new version of MiniML including "let". nipkow parents: 2031 diff changeset	9	time_use_thy "W";