isabelle: src/Sequents/Modal0.thy@0531e5abf680 (annotated)

17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	1	(* Title: Sequents/Modal0.thy
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: Martin Coen
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	*)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	6
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	7	theory Modal0
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	8	imports LK0
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	9	uses "modal.ML"
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	10	begin
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	11
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	12	consts
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	13	box :: "o=>o" ("[]_" [50] 50)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	14	dia :: "o=>o" ("<>_" [50] 50)
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	15	"--<" :: "[o,o]=>o" (infixr 25)
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	16	">-<" :: "[o,o]=>o" (infixr 25)
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	17	Lstar :: "two_seqi"
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	18	Rstar :: "two_seqi"
14765 bafb24c150c1 proper use of 'syntax'; wenzelm parents: 7098 diff changeset	19
bafb24c150c1 proper use of 'syntax'; wenzelm parents: 7098 diff changeset	20	syntax
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	21	"@Lstar" :: "two_seqe" ("(_)\|L>(_)" [6,6] 5)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	22	"@Rstar" :: "two_seqe" ("(_)\|R>(_)" [6,6] 5)
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	23
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	24	ML {*
2073 fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	25	val Lstar = "Lstar";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	26	val Rstar = "Rstar";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	27	val SLstar = "@Lstar";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	28	val SRstar = "@Rstar";
fb0655539d05 New unified treatment of sequent calculi by Sara Kalvala paulson parents: diff changeset	29
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	30	fun star_tr c [s1,s2] = Const(c,dummyT)$ seq_tr s1$ seq_tr s2;
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	31	fun star_tr' c [s1,s2] = Const(c,dummyT) $ seq_tr' s1 $ seq_tr' s2;
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	32	*}
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	33
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	34	parse_translation {* [(SLstar,star_tr Lstar), (SRstar,star_tr Rstar)] *}
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	35	print_translation {* [(Lstar,star_tr' SLstar), (Rstar,star_tr' SRstar)] *}
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	36
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	37	defs
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	38	strimp_def: "P --< Q == [](P --> Q)"
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	39	streqv_def: "P >-< Q == (P --< Q) & (Q --< P)"
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	40
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	41	ML {* use_legacy_bindings (the_context ()) *}
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	42
75166ebb619b converted to Isar theory format; wenzelm parents: 14765 diff changeset	43	end

author	wenzelm
	Mon, 01 May 2006 17:05:11 +0200
changeset 19523	0531e5abf680
parent 17481	75166ebb619b
child 21426	87ac12bed1ab
permissions	-rw-r--r--