isabelle: src/Sequents/ROOT.ML@b09a67a3dc1e (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	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	3	Copyright 1991 University of Cambridge
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	4
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 16019 diff changeset	5	Classical Sequent Calculus based on Pure Isabelle.
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	6	*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	7
24106 f2965bf954dc simultaneous use_thys; wenzelm parents: 21426 diff changeset	8	use_thys ["LK", "ILL", "ILL_predlog", "Washing", "Modal0", "T", "S4", "S43"];