Add test-case for p/printing of q-vars prefix + indented body

HOL-Theorem-Prover · Dec 31, 2017 · fa89a2b · fa89a2b
1 parent 5efbdf8
commit fa89a2b
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/num/theories/selftest.sml b/src/num/theories/selftest.sml
@@ -35,7 +35,10 @@ in
   List.app tpp [
     "case e1 of 0 => (case e2 of 0 => 1 | SUC n => n + 1) | SUC m => m * 2",
     "case e1 of 0 => 1 | SUC n => case e2 of 0 => 2 | SUC m => 3",
-    "(case x of 0 => (\\x. x) | SUC n => (\\m. m + n)) y"
+    "(case x of 0 => (\\x. x) | SUC n => (\\m. m + n)) y",
+    "!a b c d e f g.\n   \
+       \foo' a b /\\ bar a c /\\ baz a c d /\\ qux f g /\\ foo' f g ==>\n   \
+       \(a + b * c = 10 * d + e + f + g)"
   ] ;
   trace ("PP.print_firstcasebar", 1) tpp "case e of | 0 => 1 | SUC n => n + 2";
   trace ("PP.print_firstcasebar", 1) tpp