--- a/src/HOL/Nunchaku/Tools/nunchaku_problem.ML Fri Oct 28 20:41:18 2016 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_problem.ML Sat Oct 29 00:39:32 2016 +0200
@@ -107,6 +107,7 @@
val nun_match: string
val nun_mu: string
val nun_not: string
+ val nun_partial_quotient: string
val nun_pred: string
val nun_prop: string
val nun_quotient: string
@@ -280,6 +281,7 @@
val nun_match = "match";
val nun_mu = "mu";
val nun_not = "~";
+val nun_partial_quotient = "partial_quotient";
val nun_pred = "pred";
val nun_prop = "prop";
val nun_quotient = "quotient";
@@ -737,9 +739,10 @@
(case subset of
NONE => ""
| SOME s => if is_triv_subset s then "" else "\n " ^ nun_subset ^ " " ^ str_of_tm s) ^
+ (* TODO: use nun_quotient when possible *)
(case quotient of
NONE => ""
- | SOME q => "\n " ^ nun_quotient ^ " " ^ str_of_tm q) ^
+ | SOME q => "\n " ^ nun_partial_quotient ^ " " ^ str_of_tm q) ^
"\n " ^ nun_abstract ^ " " ^ str_of_tm abs ^ "\n " ^ nun_concrete ^ " " ^ str_of_tm rep;
fun str_of_nun_ctr_spec {ctr, arg_tys} =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Oct 28 20:41:18 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Sat Oct 29 00:39:32 2016 +0200
@@ -2,14 +2,16 @@
Author: Steffen Juilf Smolka, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
-Supplements term with a locally minmal, complete set of type constraints. Complete: The constraints
-suffice to infer the term's types. Minimal: Reducing the set of constraints further will make it
-incomplete.
+Supplements term with a locally minimal, complete set of type constraints.
+Complete: The constraints suffice to infer the term's types. Minimal: Reducing
+the set of constraints further will make it incomplete.
-When configuring the pretty printer appropriately, the constraints will show up as type annotations
-when printing the term. This allows the term to be printed and reparsed without a change of types.
+When configuring the pretty printer appropriately, the constraints will show up
+as type annotations when printing the term. This allows the term to be printed
+and reparsed without a change of types.
-Note: Terms should be unchecked before calling "annotate_types_in_term" to avoid awkward syntax.
+Terms should be unchecked before calling "annotate_types_in_term" to avoid
+awkward syntax.
*)
signature SLEDGEHAMMER_ISAR_ANNOTATE =