isabelle: src/Sequents/LK/ROOT.ML@89c5afe4139a (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
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 9000 diff changeset	6	Examples for Classical Logic.
6252 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";