isabelle: src/Sequents/ILL/ILL_predlog.thy@8fde30f5cca6 (annotated)

17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	1	(* $Id$ *)
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	2
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	3	theory ILL_predlog
75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	4	imports ILL
75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	5	begin
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	6
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	7	typedecl plf
75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	8
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	9	consts
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	10	"&" :: "[plf,plf] => plf" (infixr 35)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	11	"\|" :: "[plf,plf] => plf" (infixr 35)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	12	">" :: "[plf,plf] => plf" (infixr 35)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	13	"=" :: "[plf,plf] => plf" (infixr 35)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	14	"@NG" :: "plf => plf" ("- _ " [50] 55)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	15	ff :: "plf"
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	16
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	17	PL :: "plf => o" ("[* / _ / *]" [] 100)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	18
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	19
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	20	translations
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	21
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	22	"[* A & B ]" == "[A] && [B*]"
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	23	"[* A \| B ]" == "![A] ++ ![B*]"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	24	"[* - A ]" == "[A > ff*]"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	25	"[* ff *]" == "0"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	26	"[* A = B ]" => "[ (A > B) & (B > A) *]"
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	27
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	28	"[* A > B ]" == "![A] -o [B*]"
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 14854 diff changeset	29
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	30	(* another translations for linear implication:
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	31	"[* A > B ]" == "!([A] -o [B])" )
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	32
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	33	end

author	wenzelm
	Tue, 22 Nov 2005 19:34:46 +0100
changeset 18226	8fde30f5cca6
parent 17481	75166ebb619b
permissions	-rw-r--r--