isabelle: src/Sequents/LK/ROOT.ML@87ac12bed1ab (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
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	9	use_thy "Propositional";
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	10	use_thy "Quantifiers";
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	11	use_thy "Hard_Quantifiers";
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	12	use_thy "Nat";