isabelle: src/Sequents/LK/ROOT.ML@c20d58286a51 (annotated)

9000 c20d58286a51 cleaned up; wenzelm parents: 7091 diff changeset	1	(* Title: LK/ex/ROOT.ML
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	2	ID: $Id$
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	4	Copyright 1992 University of Cambridge
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	5
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	6	Executes all examples for Classical Logic.
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	7	*)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	8
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	9	time_use "prop.ML";
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	10	time_use "quant.ML";
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	11	time_use "hardquant.ML";
9000 c20d58286a51 cleaned up; wenzelm parents: 7091 diff changeset	12	time_use_thy "Nat";