Mercurial Mercurial > repos > isabelle / diff
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.
src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 35601 50ba5010b876
parent 35599 20670f5564e9
child 35630 8e562d56d404 
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 15:27:47 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Mar 05 15:59:48 2010 -0800
@@ -278,6 +278,9 @@
     val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
     val is_emptys = map warn n__eqs;
     val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
+    val _ = if is_finite
+            then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
+            else ();
   end;
   val _ = trace " Proving finite_ind...";
   val finite_ind =
isabelle