isabelle: src/Sequents/ROOT.ML@a189707c1d76 (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";
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	16
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	17	use_thy "ILL";
21426 87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	18	use_thy "ILL_predlog";
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	19	use_thy "Washing";
87ac12bed1ab converted legacy ML scripts; wenzelm parents: 17481 diff changeset	20
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	21	use_thy "Modal0";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	22	use_thy"T";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	23	use_thy"S4";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	24	use_thy"S43";

author	wenzelm
	Wed, 13 Jun 2007 00:01:57 +0200
changeset 23354	a189707c1d76
parent 21426	87ac12bed1ab
child 24106	f2965bf954dc
permissions	-rw-r--r--