--- a/NEWS Sun Jul 02 20:09:12 2023 +0200
+++ b/NEWS Sun Jul 02 20:41:07 2023 +0200
@@ -76,6 +76,9 @@
- Made clausifier more robust in the face of nested lambdas.
Minor INCOMPATIBILITY.
+* Command "try0":
+ - Add proof method "order".
+
* 'primcorec': Made the internal tactic more robust in the face of
nested corecursion.
--- a/src/HOL/Tools/try0.ML Sun Jul 02 20:09:12 2023 +0200
+++ b/src/HOL/Tools/try0.ML Sun Jul 02 20:41:07 2023 +0200
@@ -93,7 +93,8 @@
("fastforce", ((false, false), full_attrs)),
("force", ((false, false), full_attrs)),
("meson", ((false, false), metis_attrs)),
- ("satx", ((false, false), no_attrs))];
+ ("satx", ((false, false), no_attrs)),
+ ("order", ((false, true), no_attrs))];
val apply_methods = map apply_named_method named_methods;