| Tue, 18 Oct 2016 16:03:30 +0200 | wenzelm | clarified modules; | file | diff | annotate |
| Mon, 07 Mar 2016 21:09:28 +0100 | wenzelm | File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; | file | diff | annotate |
| Fri, 25 Sep 2015 20:37:59 +0200 | wenzelm | moved remaining display.ML to more_thm.ML; | file | diff | annotate |
| Sat, 18 Jul 2015 20:47:08 +0200 | wenzelm | prefer tactics with explicit context; | file | diff | annotate |
| Wed, 08 Jul 2015 19:28:43 +0200 | wenzelm | Variable.focus etc.: optional bindings provided by user; | file | diff | annotate |
| Fri, 06 Mar 2015 23:52:35 +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 |
| Thu, 28 Aug 2014 00:40:38 +0200 | blanchet | add 'old_' prefix to SMT file names; add 'Old_' to ML module names; | file | diff | annotate | base |