isabelle: src/Sequents/ILL/washing.thy@d7619ccf22e6 (annotated)

6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	1
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	2	(* $Id$ *)
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	3
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	4	(* code by Sara Kalvala, based on Paulson's LK
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	5	and Moore's tisl.ML *)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	6
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	7	theory washing
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	8	imports ILL
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	9	begin
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	10
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	11	consts
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	12	dollar :: o
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	13	quarter :: o
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	14	loaded :: o
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	15	dirty :: o
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	16	wet :: o
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	17	clean :: o
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	18
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	19	axioms
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	20	change:
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	21	"dollar \|- (quarter >< quarter >< quarter >< quarter)"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	22
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	23	load1:
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	24	"quarter , quarter , quarter , quarter , quarter \|- loaded"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	25
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	26	load2:
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	27	"dollar , quarter \|- loaded"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	28
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	29	wash:
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	30	"loaded , dirty \|- wet"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	31
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	32	dry:
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	33	"wet, quarter , quarter , quarter \|- clean"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	34
17481 75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	35	ML {* use_legacy_bindings (the_context ()) *}
75166ebb619b converted to Isar theory format; wenzelm parents: 6252 diff changeset	36
6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	37	end
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	38

author	paulson
	Fri, 14 Oct 2005 15:34:56 +0200
changeset 17849	d7619ccf22e6
parent 17481	75166ebb619b
permissions	-rw-r--r--