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

6252 935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	1
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	2
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	3	(* code by Sara Kalvala, based on Paulson's LK
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	4	and Moore's tisl.ML *)
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	5
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	6	washing = ILL +
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	7
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	8	consts
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	9
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	10	dollar,quarter,loaded,dirty,wet,clean :: "o"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	11
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	12
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	13	rules
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	14
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	15
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	16	change
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	17	"dollar \|- (quarter >< quarter >< quarter >< quarter)"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	18
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	19	load1
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	20	"quarter , quarter , quarter , quarter , quarter \|- loaded"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	21
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	22	load2
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	23	"dollar , quarter \|- loaded"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	24
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	25	wash
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	26	"loaded , dirty \|- wet"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	27
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	28	dry
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	29	"wet, quarter , quarter , quarter \|- clean"
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	30
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	31	end
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	32
935f183bf406 examples made separate dirs; wenzelm parents: diff changeset	33

author	oheimb
	Fri, 02 Jun 2000 17:46:32 +0200
changeset 9020	1056cbbaeb29
parent 6252	935f183bf406
child 17481	75166ebb619b
permissions	-rw-r--r--