src/HOL/Bali/Decl.thy
changeset 63680 6e1e8b5abbfa
parent 63648 f9f3006a5579
child 67443 3abf6a722518
equal deleted inserted replaced
63679:dc311d55ad8f 63680:6e1e8b5abbfa
    13 improvements:
    13 improvements:
    14 \begin{itemize}
    14 \begin{itemize}
    15 \item clarification and correction of some aspects of the package/access concept
    15 \item clarification and correction of some aspects of the package/access concept
    16   (Also submitted as bug report to the Java Bug Database:
    16   (Also submitted as bug report to the Java Bug Database:
    17    Bug Id: 4485402 and Bug Id: 4493343 
    17    Bug Id: 4485402 and Bug Id: 4493343 
    18    @{url "http://developer.java.sun.com/developer/bugParade/index.jshtml"}
    18    \<^url>\<open>http://developer.java.sun.com/developer/bugParade/index.jshtml\<close>
    19   )
    19   )
    20 \end{itemize}
    20 \end{itemize}
    21 simplifications:
    21 simplifications:
    22 \begin{itemize}
    22 \begin{itemize}
    23 \item the only field and method modifiers are static and the access modifiers
    23 \item the only field and method modifiers are static and the access modifiers