| Fri, 06 Mar 2015 23:56:43 +0100 | wenzelm | clarified context; | file | diff | annotate |
| Fri, 06 Mar 2015 15:58:56 +0100 | wenzelm | Thm.cterm_of and Thm.ctyp_of operate on local context; | file | diff | annotate |
| Fri, 06 Mar 2015 00:00:57 +0100 | wenzelm | tuned -- more explicit use of context; | file | diff | annotate |
| Wed, 04 Mar 2015 19:53:18 +0100 | wenzelm | tuned signature -- prefer qualified names; | file | diff | annotate |
| Tue, 03 Mar 2015 19:08:04 +0100 | traytel | eliminated some clones of Proof_Context.cterm_of | file | diff | annotate |
| Wed, 26 Nov 2014 20:05:34 +0100 | wenzelm | renamed "pairself" to "apply2", in accordance to @{apply 2}; | file | diff | annotate |
| Sun, 02 Jun 2013 10:57:21 +0200 | haftmann | denesting of functions | file | diff | annotate |
| Sun, 02 Jun 2013 07:46:40 +0200 | haftmann | make reification part of HOL | file | diff | annotate | base |