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

24584 01e83ffa6c54 fixed title haftmann parents: 24106 diff changeset	1	(* Title: Sequents/LK/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
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 21426 diff changeset	9	use_thys ["Propositional", "Quantifiers", "Hard_Quantifiers", "Nat"];
f2965bf954dc simultaneous use_thys; wenzelm parents: 21426 diff changeset	10