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

9000 c20d58286a51 cleaned up; wenzelm parents: 8011 diff changeset	1
9143 6180c29d2db6 use with_paths; wenzelm parents: 9000 diff changeset	2	goals_limit := 1;
8011 d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	3
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	4	Unify.search_bound := 40;
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	5	Unify.trace_bound := 40;
d14c4e9e9c8e * empty log message * nipkow parents: diff changeset	6
10611 e460c53c1c9b simplified interactive handling oheimb parents: 10047 diff changeset	7	add_path "J";
e460c53c1c9b simplified interactive handling oheimb parents: 10047 diff changeset	8	add_path "JVM";
e460c53c1c9b simplified interactive handling oheimb parents: 10047 diff changeset	9	add_path "BV";
e460c53c1c9b simplified interactive handling oheimb parents: 10047 diff changeset	10	use_thy "Digest";