Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed obsolete 'symbols' mode;
authorwenzelm
Thu, 01 Sep 2005 15:58:10 +0200
changeset 17218 64242b791c19
parent 17217 954c0f265203
child 17219 515badbfc4d6
removed obsolete 'symbols' mode;
src/Pure/General/symbol.ML file | annotate | diff | comparison | revisions
src/Pure/Thy/latex.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/General/symbol.ML	Thu Sep 01 15:58:08 2005 +0200
+++ b/src/Pure/General/symbol.ML	Thu Sep 01 15:58:10 2005 +0200
@@ -56,7 +56,6 @@
   val default_output: string -> string * real
   val default_indent: string * int -> string
   val default_raw: string -> string
-  val symbolsN: string
   val xsymbolsN: string
   val symbol_output: string -> string * real
 end;
@@ -488,7 +487,6 @@
 
 (* xsymbols *)
 
-val symbolsN = "symbols";    (*legacy!*)
 val xsymbolsN = "xsymbols";
 
 fun sym_len s =
--- a/src/Pure/Thy/latex.ML	Thu Sep 01 15:58:08 2005 +0200
+++ b/src/Pure/Thy/latex.ML	Thu Sep 01 15:58:10 2005 +0200
@@ -154,7 +154,7 @@
 (* print mode *)
 
 val latexN = "latex";
-val modes = [latexN, Symbol.xsymbolsN, Symbol.symbolsN];
+val modes = [latexN, Symbol.xsymbolsN];
 
 fun latex_output str =
   let val syms = Symbol.explode str
isabelle