isabelle: src/HOL/MicroJava/ROOT.ML@da6788606f54 (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
9240 f4d76cb26433 added BinOp oheimb parents: 9143 diff changeset	7	with_paths ["J" ] use_thy "JTypeSafe";
9557 c1e730bebcaa added Example oheimb parents: 9240 diff changeset	8	with_paths ["J" ] use_thy "Example";
9143 6180c29d2db6 use with_paths; wenzelm parents: 9000 diff changeset	9	with_paths ["J", "JVM", "BV"] use_thy "BVSpecTypeSafe";
9579 28e26f468f08 added LBV kleing parents: 9557 diff changeset	10	with_paths ["J", "JVM", "BV"] use_thy "LBVCorrect";
28e26f468f08 added LBV kleing parents: 9557 diff changeset	11	with_paths ["J", "JVM", "BV"] use_thy "LBVComplete";