src/HOL/MicroJava/ROOT.ML
author kleing
Thu Sep 21 12:25:48 2000 +0200 (2000-09-21)
changeset 10047 8f228c148456
parent 9579 28e26f468f08
child 10611 e460c53c1c9b
permissions -rw-r--r--
Digest.thy as toplevel theory
wenzelm@9000
     1
wenzelm@9143
     2
goals_limit := 1;
nipkow@8011
     3
nipkow@8011
     4
Unify.search_bound := 40;
nipkow@8011
     5
Unify.trace_bound  := 40;
nipkow@8011
     6
kleing@10047
     7
with_paths ["J", "JVM", "BV"] use_thy "Digest";