# HG changeset patch
# User haftmann
# Date 1236783409 -3600
# Node ID e3641cac56fa693d28595e3be8495c254d939bb4
# Parent  57c68b3af2eae3dbd04d823fbb91e18640471c9f
min_weak_def [code del]

diff -r 57c68b3af2ea -r e3641cac56fa src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Wed Mar 11 10:58:18 2009 +0100
+++ b/src/HOL/FunDef.thy	Wed Mar 11 15:56:49 2009 +0100
@@ -229,7 +229,7 @@
 definition "max_strict = max_ext pair_less"
 definition [code del]: "max_weak = max_ext pair_leq \<union> {({}, {})}"
 definition [code del]: "min_strict = min_ext pair_less"
-definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
+definition [code del]: "min_weak = min_ext pair_leq \<union> {({}, {})}"
 
 lemma wf_pair_less[simp]: "wf pair_less"
   by (auto simp: pair_less_def)
diff -r 57c68b3af2ea -r e3641cac56fa src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Wed Mar 11 10:58:18 2009 +0100
+++ b/src/HOL/ex/ExecutableContent.thy	Wed Mar 11 15:56:49 2009 +0100
@@ -24,6 +24,4 @@
   "~~/src/HOL/ex/Records"
 begin
 
-declare min_weak_def [code del]
-
 end