src/HOL/Library/Code_Abstract_Nat.thy
6 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
8 months ago wenzelm 2018-10-31 clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-12-21 wenzelm 2014-12-21 proper context;
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-06-28 haftmann 2014-06-28 proper trading of variables; more appropriate ML variable names
2014-06-28 haftmann 2014-06-28 modernized
2014-04-29 wenzelm 2014-04-29 prefer plain ASCII / latex over not-so-universal Unicode;
2014-02-26 haftmann 2014-02-26 prefer proof context over background theory
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2013-02-14 haftmann 2013-02-14 factored out shared preprocessor setup into theory Code_Abstract_Nat, tuning descriptions