equal
deleted
inserted
replaced
96 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within 
96 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within 
97 a proof context. 
97 a proof context. 
98 
98 
99 * Proper output of antiquotations for theory commands involving a 
99 * Proper output of antiquotations for theory commands involving a 
100 proof context (such as 'locale' or 'theorem (in loc) ...'). 
100 proof context (such as 'locale' or 'theorem (in loc) ...'). 

101 

102 * Delimiters of outer tokens (string etc.) now produce separate LaTeX 

103 macros (\isachardoublequoteopen, isachardoublequoteclose etc.). 

104 

105 * isatool usedir: new option C (default true) controls whether option 

106 D should include a copy of the original document directory; C false 

107 prevents unwanted effects such as copying of administrative CVS data. 
101 
108 
102 
109 
103 *** Pure *** 
110 *** Pure *** 
104 
111 
105 * Considerably improved version of 'constdefs' command. Now performs 
112 * Considerably improved version of 'constdefs' command. Now performs 
590 Theory.merge, etc.) 
597 Theory.merge, etc.) 
591 
598 
592 The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm 
599 The most basic sign_of operations (Theory.sign_of, Thm.sign_of_thm 
593 etc.) as well as the sign field in Thm.rep_thm etc. have been retained 
600 etc.) as well as the sign field in Thm.rep_thm etc. have been retained 
594 for convenience  they merely return the theory. 
601 for convenience  they merely return the theory. 

602 

603 * Pure: type Type.tsig is superceded by theory in most interfaces. 
595 
604 
596 * Pure: the Isar proof context type is already defined early in Pure 
605 * Pure: the Isar proof context type is already defined early in Pure 
597 as Context.proof (note that ProofContext.context and Proof.context are 
606 as Context.proof (note that ProofContext.context and Proof.context are 
598 aliases, where the latter is the preferred name). This enables other 
607 aliases, where the latter is the preferred name). This enables other 
599 Isabelle components to refer to that type even before Isar is present. 
608 Isabelle components to refer to that type even before Isar is present. 