src/HOL/HOL.thy
changeset 27107 4a7415c67063
parent 26957 e3f04fdd994d
child 27126 3ede9103de8e
     1.1 --- a/src/HOL/HOL.thy	Tue Jun 10 15:30:56 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Jun 10 15:30:58 2008 +0200
     1.3 @@ -29,7 +29,6 @@
     1.4    "~~/src/Tools/code/code_funcgr.ML"
     1.5    "~~/src/Tools/code/code_thingol.ML"
     1.6    "~~/src/Tools/code/code_target.ML"
     1.7 -  "~~/src/Tools/code/code_package.ML"
     1.8    "~~/src/Tools/nbe.ML"
     1.9  begin
    1.10  
    1.11 @@ -279,10 +278,6 @@
    1.12    greater  (infix ">" 50) where
    1.13    "x > y \<equiv> y < x"
    1.14  
    1.15 -definition
    1.16 -  Least :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" (binder "LEAST " 10) where
    1.17 -  "Least P == (THE x. P x \<and> (\<forall>y. P y \<longrightarrow> less_eq x y))"
    1.18 -
    1.19  end
    1.20  
    1.21  syntax