# HG changeset patch
# User wenzelm
# Date 1452548060 -3600
# Node ID e410c628710374e0e8af623048e4f2fc44175f5c
# Parent  a1b666aaac1a20964792f3555d9104fc4dc428b7
eliminated old defs;

diff -r a1b666aaac1a -r e410c6287103 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Mon Jan 11 22:30:18 2016 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Mon Jan 11 22:34:20 2016 +0100
@@ -894,10 +894,20 @@
 
 consts inverse :: "'a \<Rightarrow> 'a"
 
-defs (overloaded)
-  inverse_bool: "inverse (b::bool)   == ~ b"
-  inverse_set : "inverse (S::'a set) == -S"
-  inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"
+overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
+begin
+  definition "inverse (b::bool) \<equiv> \<not> b"
+end
+
+overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
+begin
+  definition "inverse (S::'a set) \<equiv> -S"
+end
+
+overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> 'b"
+begin
+  definition "inverse_pair p \<equiv> (inverse (fst p), inverse (snd p))"
+end
 
 lemma "inverse b"
 refute [expect = genuine]