src/HOL/HOL.thy
changeset 41865 4e8483cc2cc5
parent 41827 98eda7ffde79
child 42057 3eba96ff3d3e
     1.1 --- a/src/HOL/HOL.thy	Fri Feb 25 12:16:18 2011 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Feb 28 15:06:36 2011 +0000
     1.3 @@ -908,6 +908,8 @@
     1.4  declare ex_ex1I [rule del, intro! 2]
     1.5    and ex1I [intro]
     1.6  
     1.7 +declare ext [intro]
     1.8 +
     1.9  lemmas [intro?] = ext
    1.10    and [elim?] = ex1_implies_ex
    1.11