src/Pure/Isar/code.ML
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-12-02 haftmann 2009-12-02 crude support for type aliasses and corresponding constant signatures
2009-11-19 bulwahn 2009-11-19 replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
2009-11-16 haftmann 2009-11-16 proper purge
2009-11-09 haftmann 2009-11-09 tuned error messages; tuned code
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-29 wenzelm 2009-10-29 modernized functor/structures Interpretation;
2009-10-22 haftmann 2009-10-22 close thm derivations explicitly
2009-10-19 haftmann 2009-10-19 dropped lazy code equations
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
2009-10-14 haftmann 2009-10-14 sharpened name
2009-10-14 haftmann 2009-10-14 more explicit notion of canonized code equations
2009-10-05 haftmann 2009-10-05 tuned handling of type variable names further
2009-10-05 haftmann 2009-10-05 variables in type schemes must be renamed simultaneously with variables in equations
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-23 bulwahn 2009-09-23 handling of definitions
2009-09-23 bulwahn 2009-09-23 experimenting to add some useful interface for definitions
2009-09-22 haftmann 2009-09-22 corrected order of type variables in code equations; more precise certificate for cases
2009-09-09 haftmann 2009-09-09 moved eq handling in nbe into separate oracle
2009-08-10 haftmann 2009-08-10 same_typscheme replaces ugly common_typ_eqns
2009-07-31 haftmann 2009-07-31 using certify_instantiate
2009-07-31 haftmann 2009-07-31 cleaned up variable desymbolification and argument expansion
2009-07-22 wenzelm 2009-07-22 merged, resolving trivial conflict;
2009-07-21 haftmann 2009-07-21 more accurate check of judgment type
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-14 haftmann 2009-07-14 clarified code
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-07-08 haftmann 2009-07-08 tuned structure Code internally
2009-07-07 haftmann 2009-07-07 tuned interface of structure Code
2009-06-30 haftmann 2009-06-30 an intermediate step towards a refined translation of cases
2009-06-15 haftmann 2009-06-15 permissive code attribute; all_eqns
2009-06-09 haftmann 2009-06-09 tuned make/map/merge combinators
2009-05-14 haftmann 2009-05-14 merged module code_unit.ML into code.ML
2009-05-14 haftmann 2009-05-14 strip sorts while checking pattern subsumption
2009-05-12 haftmann 2009-05-12 transferred code generator preprocessor into separate module
2009-05-11 haftmann 2009-05-11 corrected deletetion of code equations for constructors
2009-05-11 haftmann 2009-05-11 clarified matter of "proper" flag in code equations
2009-05-11 haftmann 2009-05-11 clarified terminilogy concerning nbe equations
2009-04-15 haftmann 2009-04-15 say farewell to code related to old code_funcgr module
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-08 wenzelm 2009-03-08 proper context for Simplifier.pretty_ss;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-23 haftmann 2009-02-23 improved treatment of case certificates
2009-02-22 haftmann 2009-02-22 subalgebra: drop arities if desired
2009-02-20 haftmann 2009-02-20 permissive check for pattern discipline in case schemes
2009-02-18 haftmann 2009-02-18 tuned accessor name
2009-01-01 wenzelm 2009-01-01 normalized some ML type/val aliases;
2008-12-04 wenzelm 2008-12-04 renamed type Lazy.T to lazy;
2008-10-29 haftmann 2008-10-29 explicit check for pattern discipline before code translation
2008-10-28 haftmann 2008-10-28 cleanup code default attribute
2008-10-27 haftmann 2008-10-27 explicit history for equations; tuned
2008-10-23 wenzelm 2008-10-23 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
2008-10-23 wenzelm 2008-10-23 adapted Susp.peek;
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-07 haftmann 2008-10-07 clarified preprocessor policies