isabelle: src/LCF/ex/ROOT.ML@4c57e850e8d5 (annotated)

4905 be73ddff6c5a proper thy files; wenzelm parents: 4446 diff changeset	1	(* Title: LCF/ex/ROOT.ML
be73ddff6c5a proper thy files; wenzelm parents: 4446 diff changeset	2	ID: $Id$
be73ddff6c5a proper thy files; wenzelm parents: 4446 diff changeset	3	Author: Tobias Nipkow
be73ddff6c5a proper thy files; wenzelm parents: 4446 diff changeset	4	Copyright 1991 University of Cambridge
be73ddff6c5a proper thy files; wenzelm parents: 4446 diff changeset	5
15661 9ef583b08647 reverted renaming of Some/None in comments and strings; wenzelm parents: 15531 diff changeset	6	Some examples from Lawrence Paulson's book Logic and Computation.
4905 be73ddff6c5a proper thy files; wenzelm parents: 4446 diff changeset	7	*)
2820 6303966dce96 replaced ex.ML by ex/ROOT.ML, ex/ex.ML; wenzelm parents: diff changeset	8
9000 c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	9	time_use_thy "Ex1";
c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	10	time_use_thy "Ex2";
c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	11	time_use_thy "Ex3";
c20d58286a51 cleaned up; wenzelm parents: 6349 diff changeset	12	time_use_thy "Ex4";