isabelle: src/Sequents/ROOT.ML@550e36c6a2d1 (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
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	9	val banner = "Sequent Calculii";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	10	writeln banner;
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	11
7120 6d5923cecece sequents require higher bounds paulson parents: 7098 diff changeset	12	Unify.trace_bound:= 20;
6d5923cecece sequents require higher bounds paulson parents: 7098 diff changeset	13	Unify.search_bound := 40;
6d5923cecece sequents require higher bounds paulson parents: 7098 diff changeset	14
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	15	use_thy "LK";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	16	use_thy "ILL";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	17	use_thy "Modal0";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	18	use_thy"T";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	19	use_thy"S4";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	20	use_thy"S43";

author	wenzelm
	Wed, 19 Jul 2006 12:12:03 +0200
changeset 20160	550e36c6a2d1
parent 17481	75166ebb619b
child 21426	87ac12bed1ab
permissions	-rw-r--r--