isabelle: src/HOL/MicroJava/ROOT.ML@a47f51daa6dc (annotated)

9143 6180c29d2db6 use with_paths; wenzelm parents: 9000 diff changeset	1	goals_limit := 1;
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	2
10611 e460c53c1c9b simplified interactive handling oheimb parents: 10047 diff changeset	3	add_path "J";
e460c53c1c9b simplified interactive handling oheimb parents: 10047 diff changeset	4	add_path "JVM";
e460c53c1c9b simplified interactive handling oheimb parents: 10047 diff changeset	5	add_path "BV";
10631 591ea23d27a0 removed Digest (temporarily, not up to date) kleing parents: 10611 diff changeset	6
12773 a47f51daa6dc use exec_lub instead of some_lub kleing parents: 12522 diff changeset	7	use_thy "JVMType"
a47f51daa6dc use exec_lub instead of some_lub kleing parents: 12522 diff changeset	8	use_thy "JVMExceptions"
a47f51daa6dc use exec_lub instead of some_lub kleing parents: 12522 diff changeset	9
a47f51daa6dc use exec_lub instead of some_lub kleing parents: 12522 diff changeset	10	(*
10631 591ea23d27a0 removed Digest (temporarily, not up to date) kleing parents: 10611 diff changeset	11	use_thy "JTypeSafe";
591ea23d27a0 removed Digest (temporarily, not up to date) kleing parents: 10611 diff changeset	12	use_thy "Example";
12441 c586d08520ad Added examples for code generator. berghofe parents: 11070 diff changeset	13	use_thy "JListExample";
12522 69971d68fe03 fixed JVMListExample kleing parents: 12520 diff changeset	14	use_thy "JVMListExample";
10631 591ea23d27a0 removed Digest (temporarily, not up to date) kleing parents: 10611 diff changeset	15	use_thy "BVSpecTypeSafe";
12520 6d754b9a1303 temporarily removed JVMListExample kleing parents: 12441 diff changeset	16	use_thy "JVM";
6d754b9a1303 temporarily removed JVMListExample kleing parents: 12441 diff changeset	17	use_thy "LBVSpec";
12773 a47f51daa6dc use exec_lub instead of some_lub kleing parents: 12522 diff changeset	18	*)
12520 6d754b9a1303 temporarily removed JVMListExample kleing parents: 12441 diff changeset	19	(* momentarily broken:
10631 591ea23d27a0 removed Digest (temporarily, not up to date) kleing parents: 10611 diff changeset	20	use_thy "LBVCorrect";
591ea23d27a0 removed Digest (temporarily, not up to date) kleing parents: 10611 diff changeset	21	use_thy "LBVComplete";
12520 6d754b9a1303 temporarily removed JVMListExample kleing parents: 12441 diff changeset	22	*)

author	kleing
	Tue, 15 Jan 2002 22:22:05 +0100
changeset 12773	a47f51daa6dc
parent 12522	69971d68fe03
child 12786	d655138ddadf
permissions	-rw-r--r--