equal
deleted
inserted
replaced
54 \<^path>\<open>Markup.hs\<close>, |
54 \<^path>\<open>Markup.hs\<close>, |
55 \<^path>\<open>XML.hs\<close>, |
55 \<^path>\<open>XML.hs\<close>, |
56 \<^path>\<open>XML/Encode.hs\<close>, |
56 \<^path>\<open>XML/Encode.hs\<close>, |
57 \<^path>\<open>XML/Decode.hs\<close>, |
57 \<^path>\<open>XML/Decode.hs\<close>, |
58 \<^path>\<open>YXML.hs\<close>, |
58 \<^path>\<open>YXML.hs\<close>, |
|
59 \<^path>\<open>Pretty.hs\<close>, |
59 \<^path>\<open>Term.hs\<close>, |
60 \<^path>\<open>Term.hs\<close>, |
60 \<^path>\<open>Term_XML/Encode.hs\<close>, |
61 \<^path>\<open>Term_XML/Encode.hs\<close>, |
61 \<^path>\<open>Term_XML/Decode.hs\<close>]; |
62 \<^path>\<open>Term_XML/Decode.hs\<close>]; |
62 |
63 |
63 val master_dir = Resources.master_directory \<^theory>; |
64 val master_dir = Resources.master_directory \<^theory>; |