src/Pure/Isar/code.ML
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-19 haftmann 2010-04-19 more appropriate representation of valid positions for abstractors; more accurate checking of abstype certificates
2010-04-19 haftmann 2010-04-19 explicit check sorts in abstract certificates; abstractor is part of dependencies
2010-04-13 haftmann 2010-04-13 more accurate pattern match
2010-04-11 haftmann 2010-04-11 user interface for abstract datatypes is an attribute, not a command
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-07 wenzelm 2010-03-07 modernized structure Local_Defs;
2010-02-26 haftmann 2010-02-26 use abstract code cerficates for bare code theorems
2010-02-24 haftmann 2010-02-24 bound argument for abstype proposition
2010-02-24 haftmann 2010-02-24 more precise exception handler
2010-02-22 haftmann 2010-02-22 more accurate when registering new types
2010-02-22 haftmann 2010-02-22 proper distinction of code datatypes and abstypes
2010-02-19 haftmann 2010-02-19 a simple concept for datatype invariants
2010-01-14 haftmann 2010-01-14 printing of cases
2010-01-13 haftmann 2010-01-13 explicit abstract type of code certificates
2010-01-13 haftmann 2010-01-13 corrected error messages; tuned
2010-01-12 haftmann 2010-01-12 code certificates as integral part of code generation
2010-01-11 haftmann 2010-01-11 added code certificates
2010-01-05 haftmann 2010-01-05 avoid exporting Type.build_tsig
2010-01-04 haftmann 2010-01-04 code cache only persists on equal theories
2010-01-04 haftmann 2010-01-04 code cache without copy; tuned
2009-12-24 haftmann 2009-12-24 made sml/nj happy
2009-12-23 haftmann 2009-12-23 reduced code generator cache to the baremost minimum
2009-12-04 wenzelm 2009-12-04 merged, resolving minor conflict, and recovering sane state;
2009-12-04 wenzelm 2009-12-04 merged, resolving minor conflicts;
2009-12-04 haftmann 2009-12-04 merged
2009-11-30 haftmann 2009-11-30 dropped some unused bindings
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
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