Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned msgs;
authorwenzelm
Tue, 29 Feb 2000 20:51:43 +0100
changeset 8315 c9b4f1c47816
parent 8314 463f63a9a7f2
child 8316 74639e19eca0
tuned msgs;
src/HOL/Tools/induct_method.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/induct_method.ML	Tue Feb 29 10:57:30 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Tue Feb 29 20:51:43 2000 +0100
@@ -38,7 +38,7 @@
 
 fun print_rules kind rs =
   let val thms = map snd (NetRules.rules rs)
-  in Pretty.writeln (Pretty.big_list (kind ^ " rules:") (map Display.pretty_thm thms)) end;
+  in Pretty.writeln (Pretty.big_list kind (map Display.pretty_thm thms)) end;
 
 
 (* theory data kind 'HOL/induct_method' *)
@@ -57,10 +57,10 @@
       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
 
   fun print _ ((casesT, casesS), (inductT, inductS)) =
-    (print_rules "type cases" casesT;
-      print_rules "set cases" casesS;
-      print_rules "type induct" inductT;
-      print_rules "set induct" inductS);
+    (print_rules "type cases:" casesT;
+      print_rules "set cases:" casesS;
+      print_rules "type induct:" inductT;
+      print_rules "set induct:" inductS);
 end;
 
 structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
isabelle