isabelle: src/Sequents/ROOT.ML@29a0e3be0be1 (annotated)

9000 c20d58286a51 cleaned up; wenzelm parents: 7120 diff changeset	1	(* Title: Sequents/ROOT.ML
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	2	ID: $Id$
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	4	Copyright 1991 University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	5
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 16019 diff changeset	6	Classical Sequent Calculus based on Pure Isabelle.
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	7	*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	8
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 21426 diff changeset	9	use_thys ["LK", "ILL", "ILL_predlog", "Washing", "Modal0", "T", "S4", "S43"];