| changeset 54890 | cb892d835803 |
| parent 54863 | 82acc20ded73 |
| child 55719 | cdddd073bff8 |
--- a/src/HOL/Real_Vector_Spaces.thy Wed Jan 01 01:05:46 2014 +0100 +++ b/src/HOL/Real_Vector_Spaces.thy Wed Jan 01 01:05:48 2014 +0100 @@ -968,7 +968,7 @@ end -code_abort "open :: real set \<Rightarrow> bool" +declare [[code abort: "open :: real set \<Rightarrow> bool"]] instance real :: linorder_topology proof