Mon, 02 Apr 2012 16:35:09 +0200 | wenzelm | refined define/abbrev: allow extra fixes in aux. context vs. bottom target (NB: export_term expands defined variables, leaving fixed ones); | changeset | files |
Mon, 02 Apr 2012 15:42:50 +0200 | wenzelm | more general Local_Theory.restore, allow any nesting level; | changeset | files |