isabelle: src/HOL/MiniML/ROOT.ML@0ccea141409b (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$
2031 03a843f0f447 Ran expandshort paulson parents: 1925 diff changeset	3	Author: 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
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
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	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	nipkow
	Fri, 17 Jan 1997 18:32:24 +0100
changeset 2523	0ccea141409b
parent 2031	03a843f0f447
child 2525	477c05586286
permissions	-rw-r--r--