Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/Essential.thy
changeset 423 0a25b35178c3
parent 418 1d1e4cda8c54
child 429 d04d1cd0e058
equal deleted inserted replaced
422:e79563b14b0f 423:0a25b35178c3 
  1080   unification. Only in case of failure full higher-order unification is
 
  1080   unification. Only in case of failure full higher-order unification is
 
  1081   called. This function has a built-in bound, which can be accessed and
 
  1081   called. This function has a built-in bound, which can be accessed and
 
  1082   manipulated as a configuration value:
 
  1082   manipulated as a configuration value:
 
  1083 
  1083 
  1084   @{ML_response_fake [display,gray]
 
  1084   @{ML_response_fake [display,gray]
 
  1085   "Config.get_thy @{theory} (Unify.search_bound_value)"
 
  1085   "Config.get_global @{theory} (Unify.search_bound_value)"
 
  1086   "Int 60"}
 
  1086   "Int 60"}
 
  1087 
  1087 
  1088   If this bound is reached during unification, Isabelle prints out the
 
  1088   If this bound is reached during unification, Isabelle prints out the
 
  1089   warning message @{text [quotes] "Unification bound exceeded"} and
 
  1089   warning message @{text [quotes] "Unification bound exceeded"} and
 
  1090   plenty of diagnostic information (sometimes annoyingly plenty of 
  1090   plenty of diagnostic information (sometimes annoyingly plenty of
isabelle-cookbook