isabelle: src/Sequents/ROOT.ML@bd641d927437 (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
	Fri, 24 Nov 2006 22:05:18 +0100
changeset 21522	bd641d927437
parent 21426	87ac12bed1ab
child 24106	f2965bf954dc
permissions	-rw-r--r--