isabelle: src/Sequents/LK/ROOT.ML@af3ff2ba4c54 (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	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	3	Copyright 1992 University of Cambridge
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	4
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 9000 diff changeset	5	Examples for Classical Logic.
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	6	*)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	7
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 21426 diff changeset	8	use_thys ["Propositional", "Quantifiers", "Hard_Quantifiers", "Nat"];
f2965bf954dc simultaneous use_thys; wenzelm parents: 21426 diff changeset	9