equal
deleted
inserted
replaced
860 \<close> |
860 \<close> |
861 |
861 |
862 class empty = |
862 class empty = |
863 assumes bad: "\<And>(x::'a) y. x \<noteq> y" |
863 assumes bad: "\<And>(x::'a) y. x \<noteq> y" |
864 |
864 |
|
865 declare [[pending_shyps]] |
|
866 |
865 theorem (in empty) false: False |
867 theorem (in empty) false: False |
866 using bad by blast |
868 using bad by blast |
|
869 |
|
870 declare [[pending_shyps = false]] |
867 |
871 |
868 ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close> |
872 ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close> |
869 |
873 |
870 text \<open> |
874 text \<open> |
871 Thanks to the inference kernel managing sort hypothesis according to their |
875 Thanks to the inference kernel managing sort hypothesis according to their |