--- a/NEWS Sat Mar 17 00:17:30 2012 +0100
+++ b/NEWS Sat Mar 17 09:51:18 2012 +0100
@@ -48,6 +48,10 @@
*** Pure ***
+* Command 'definition' no longer exports the foundational "raw_def"
+into the user context. Minor INCOMPATIBILITY, may use the regular
+"def" result with attribute "abs_def" to imitate the old version.
+
* Attribute "abs_def" turns an equation of the form "f x y == t" into
"f == %x y. t", which ensures that "simp" or "unfold" steps always
expand it. This also works for object-logic equality. (Formerly
--- a/src/HOL/Orderings.thy Sat Mar 17 00:17:30 2012 +0100
+++ b/src/HOL/Orderings.thy Sat Mar 17 09:51:18 2012 +0100
@@ -1314,7 +1314,6 @@
definition
[no_atp]: "\<top> = (\<lambda>x. \<top>)"
-declare top_fun_def_raw [no_atp]
lemma top_apply [simp] (* CANDIDATE [code] *):
"\<top> x = \<top>"
--- a/src/HOL/Quickcheck.thy Sat Mar 17 00:17:30 2012 +0100
+++ b/src/HOL/Quickcheck.thy Sat Mar 17 09:51:18 2012 +0100
@@ -262,16 +262,17 @@
where "map f P = bind P (single o f)"
hide_fact
- random_bool_def random_bool_def_raw
- random_itself_def random_itself_def_raw
- random_char_def random_char_def_raw
- random_literal_def random_literal_def_raw
- random_nat_def random_nat_def_raw
- random_int_def random_int_def_raw
- random_fun_lift_def random_fun_lift_def_raw
- random_fun_def random_fun_def_raw
- collapse_def collapse_def_raw
- beyond_def beyond_def_raw beyond_zero
+ random_bool_def
+ random_itself_def
+ random_char_def
+ random_literal_def
+ random_nat_def
+ random_int_def
+ random_fun_lift_def
+ random_fun_def
+ collapse_def
+ beyond_def
+ beyond_zero
random_aux_rec
hide_const (open) catch_match random collapse beyond random_fun_aux random_fun_lift
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Mar 17 00:17:30 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Mar 17 09:51:18 2012 +0100
@@ -867,8 +867,7 @@
(not (Config.get ctxt ignore_no_atp) andalso
is_package_def name0) orelse
exists (fn s => String.isSuffix s name0)
- (multi_base_blacklist ctxt ho_atp) orelse
- String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
+ (multi_base_blacklist ctxt ho_atp)) then
I
else
let