NEWS
changeset 16856 6468a5d6a16e
parent 16799 978dcf30c3dd
child 16860 43abdba4da5c
equal deleted inserted replaced
16855:7563d0eb3414 16856:6468a5d6a16e
   102 interpreted in the same manner as for the 'syntax' command.
   102 interpreted in the same manner as for the 'syntax' command.
   103 
   103 
   104 * 'Advanced' translation functions (parse_translation etc.) may depend
   104 * 'Advanced' translation functions (parse_translation etc.) may depend
   105 on the signature of the theory context being presently used for
   105 on the signature of the theory context being presently used for
   106 parsing/printing, see also isar-ref manual.
   106 parsing/printing, see also isar-ref manual.
       
   107 
       
   108 * Improved 'oracle' command provides a type-safe interface to turn an
       
   109 ML expression of type theory -> T -> term into a primitive rule of
       
   110 type theory -> T -> thm (i.e. the functionality of Thm.invoke_oracle
       
   111 is already included here); see also FOL/ex/IffExample.thy;
       
   112 INCOMPATIBILITY.
   107 
   113 
   108 * Improved internal renaming of symbolic identifiers -- attach primes
   114 * Improved internal renaming of symbolic identifiers -- attach primes
   109 instead of base 26 numbers.
   115 instead of base 26 numbers.
   110 
   116 
   111 * New flag show_question_marks controls printing of leading question
   117 * New flag show_question_marks controls printing of leading question