2008-11-13 haftmann 2008-11-13 moved assert to Heap_Monad.thy
2008-11-13 haftmann 2008-11-13 simproc for let
2008-11-13 haftmann 2008-11-13 improved handling of !!/==> for eval and normalization
2008-11-13 haftmann 2008-11-13 proper name morphisms for locales
2008-11-13 haftmann 2008-11-13 consider prefixes for name bindings of simprocs (a first approximation)
2008-11-13 haftmann 2008-11-13 diagnostic output for name bindings
2008-11-13 berghofe 2008-11-13 Some modifications in code for proving arities to make it work for datatype definitions with additional sort constraints.
2008-11-12 krauss 2008-11-12 min_ext/max_ext lifting wellfounded relations on finite sets. Preserves wf
2008-11-10 haftmann 2008-11-10 restruced naming code in anticipation of introduction of name morphisms
2008-11-10 haftmann 2008-11-10 more verbose element printing
2008-11-10 haftmann 2008-11-10 clarified comment
2008-11-10 berghofe 2008-11-10 Added support for parametric datatypes.
2008-11-10 berghofe 2008-11-10 Streamlined functions for accessing information about atoms.
2008-11-10 berghofe 2008-11-10 Some more functions for accessing information about atoms.
2008-11-10 ballarin 2008-11-10 Made doc compatible with the system.
2008-11-10 haftmann 2008-11-10 clarified verbatim vs. typewriter
2008-11-10 haftmann 2008-11-10 using explicit interpretaton prefix in Name.binding (still on the surface)
2008-11-10 haftmann 2008-11-10 explicit interpretation prefix in Name.binding
2008-11-10 haftmann 2008-11-10 tuned
2008-11-07 haftmann 2008-11-07 exported codegen_preproc
2008-11-06 ballarin 2008-11-06 Minor cleanup.
2008-11-06 ballarin 2008-11-06 Keyword 'includes' gone.
2008-11-06 nipkow 2008-11-06 tuned
2008-11-06 nipkow 2008-11-06 added lemma
2008-11-06 nipkow 2008-11-06 Added second tiling example.
2008-11-06 haftmann 2008-11-06 cleaned
2008-11-06 haftmann 2008-11-06 tuned
2008-11-06 haftmann 2008-11-06 class morphism stemming from locale interpretation
2008-11-03 haftmann 2008-11-03 improved verbatim mechanism
2008-10-31 berghofe 2008-10-31 Theorem "_" is now stored with open derivation.
2008-10-31 berghofe 2008-10-31 Removed argument prf2 in rewrite rules for equal_elim to make them applicable to eta-contracted proofs.
2008-10-31 berghofe 2008-10-31 Replaced arbitrary by undefined.
2008-10-30 ballarin 2008-10-30 Dropped context element 'includes'.
2008-10-29 haftmann 2008-10-29 adapted to strict pattern discipline
2008-10-29 haftmann 2008-10-29 explicit check for pattern discipline before code translation
2008-10-28 ballarin 2008-10-28 Revoked workaround (incompatible with HOL/ex/LocaleTest2.thy).
2008-10-28 haftmann 2008-10-28 restored incremental code generation
2008-10-28 haftmann 2008-10-28 slightly tuned
2008-10-28 haftmann 2008-10-28 assert that no class parameter is used as constructor
2008-10-28 haftmann 2008-10-28 cleanup code default attribute
2008-10-28 haftmann 2008-10-28 removed includes
2008-10-28 haftmann 2008-10-28 making SMLNJ happy
2008-10-28 paulson 2008-10-28 The metis method no longer fails because the theorem is too trivial
2008-10-28 ballarin 2008-10-28 Removed 'includes meta_term_syntax' and 'includes meta_conjunction_syntax'.
2008-10-27 paulson 2008-10-27 metis proof
2008-10-27 ballarin 2008-10-27 New-style locale expressions with instantiation (new file expression.ML).
2008-10-27 ballarin 2008-10-27 Hide path in constant name (workaround).
2008-10-27 haftmann 2008-10-27 explicit history for equations; tuned
2008-10-27 haftmann 2008-10-27 slightly tuned
2008-10-27 haftmann 2008-10-27 added rudimentary code generation
2008-10-27 haftmann 2008-10-27 sup_bot and inf_top
2008-10-27 ballarin 2008-10-27 Extension of interface: declarations_of.
2008-10-24 haftmann 2008-10-24 simplified user-defined class syntax
2008-10-24 haftmann 2008-10-24 more clever module names for code generation
2008-10-24 haftmann 2008-10-24 "fun" gained a more uniform status
2008-10-24 haftmann 2008-10-24 simplified syntax for class parameters
2008-10-24 haftmann 2008-10-24 tuned
2008-10-24 haftmann 2008-10-24 new classes "top" and "bot"
2008-10-24 haftmann 2008-10-24 tuned proof
2008-10-24 haftmann 2008-10-24 more clever module name aliasses for code generation