| changeset 58826 | 2ed2eaabe3df |
| parent 58813 | 625d04d4fd2a |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Quickcheck_Narrowing.thy Wed Oct 29 17:01:44 2014 +0100 +++ b/src/HOL/Quickcheck_Narrowing.thy Wed Oct 29 19:01:49 2014 +0100 @@ -197,8 +197,6 @@ ML_file "Tools/Quickcheck/narrowing_generators.ML" -setup Narrowing_Generators.setup - definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term" where "narrowing_dummy_partial_term_of = partial_term_of"