| Wed, 22 Aug 2012 22:55:41 +0200 | wenzelm | prefer ML_file over old uses; | file | diff | annotate |
| Mon, 27 Feb 2012 16:56:25 +0100 | wenzelm | more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile); | file | diff | annotate |
| Sat, 16 Apr 2011 16:15:37 +0200 | wenzelm | modernized structure Proof_Context; | file | diff | annotate |
| Mon, 20 Sep 2010 16:05:25 +0200 | wenzelm | renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; | file | diff | annotate |
| Sat, 28 Aug 2010 16:14:32 +0200 | haftmann | formerly unnamed infix equality now named HOL.eq | file | diff | annotate |
| Fri, 27 Aug 2010 10:56:46 +0200 | haftmann | formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj | file | diff | annotate |
| Mon, 03 May 2010 14:25:56 +0200 | wenzelm | renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing; | file | diff | annotate |