src/Doc/Implementation/Logic.thy
changeset 68558 7aae213d9e69
parent 68540 000a0e062529
child 69307 196347d2fd2d
     1.1 --- a/src/Doc/Implementation/Logic.thy	Sun Jul 01 12:37:24 2018 +0200
     1.2 +++ b/src/Doc/Implementation/Logic.thy	Sun Jul 01 12:38:37 2018 +0200
     1.3 @@ -862,13 +862,9 @@
     1.4  class empty =
     1.5    assumes bad: "\<And>(x::'a) y. x \<noteq> y"
     1.6  
     1.7 -declare [[pending_shyps]]
     1.8 -
     1.9  theorem (in empty) false: False
    1.10    using bad by blast
    1.11  
    1.12 -declare [[pending_shyps = false]]
    1.13 -
    1.14  ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
    1.15  
    1.16  text \<open>