src/Doc/Implementation/Logic.thy
changeset 68540 000a0e062529
parent 67146 909dcdec2122
child 68558 7aae213d9e69
     1.1 --- a/src/Doc/Implementation/Logic.thy	Fri Jun 29 14:19:52 2018 +0200
     1.2 +++ b/src/Doc/Implementation/Logic.thy	Fri Jun 29 15:54:41 2018 +0200
     1.3 @@ -862,9 +862,13 @@
     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>