2007-09-21 wenzelm 2007-09-21 added has_abs (from envir.ML);
2007-09-21 wenzelm 2007-09-21 Term.has_abs;
2007-09-21 wenzelm 2007-09-21 proper signature constraint; minor tuning;
2007-09-20 wenzelm 2007-09-20 added interrupt_timeout; tuned signature;
2007-09-20 wenzelm 2007-09-20 Generic interpretation of theory data.
2007-09-20 wenzelm 2007-09-20 tuned signature; moved generic interpretation to interpretation.ML; added abstract at_begin/end wrappers;
2007-09-20 wenzelm 2007-09-20 avoid Theory.rep_theory;
2007-09-20 wenzelm 2007-09-20 added interpretation.ML;
2007-09-20 wenzelm 2007-09-20 improved error behaviour of use (bootstrap version);
2007-09-20 haftmann 2007-09-20 more precise treatment of free dictionary parameters for evaluation
2007-09-20 haftmann 2007-09-20 fixed cg setup
2007-09-20 haftmann 2007-09-20 restored ml system independence
2007-09-20 haftmann 2007-09-20 more permissive
2007-09-20 haftmann 2007-09-20 clarified code lemmas
2007-09-20 haftmann 2007-09-20 fixed wrong syntax treatment in class target
2007-09-20 haftmann 2007-09-20 code lemmas for cardinality
2007-09-20 berghofe 2007-09-20 - eval_term no longer computes result during compile time - generated ML code is now compiled via ML_Context.use_mltext rather than use_text; this makes sure that antiquotations are expanded - quickcheck now checks whether types to be substituted for type variables have correct sorts; this avoids spurious counterexamples - execution time for auto_quickcheck is now limited
2007-09-20 obua 2007-09-20 improved computing
2007-09-20 obua 2007-09-20 changed lemmas
2007-09-19 wenzelm 2007-09-19 ml_output: proper error instead of error_msg;
2007-09-19 webertj 2007-09-19 comment added to explain a potential scheduling problem
2007-09-19 nipkow 2007-09-19 tuned
2007-09-19 nipkow 2007-09-19 *** empty log message ***
2007-09-19 paulson 2007-09-19 metis too slow
2007-09-19 isatest 2007-09-19 move at-sml-dev to 2-processor atbroy100
2007-09-19 isatest 2007-09-19 make sun-sml-dev non-proof-term, and at-sml-def -p 2 (at-sml-dev being moved to faster atbroy100)
2007-09-19 nipkow 2007-09-19 Generalized [_.._] from nat to linear orders
2007-09-19 berghofe 2007-09-19 Enclosed end_theory in text antiquotation to make LaTeX happy.
2007-09-19 wenzelm 2007-09-19 * ML: just one true type int;
2007-09-18 ballarin 2007-09-18 New diagnostic command print_orders.
2007-09-18 ballarin 2007-09-18 Transitivity reasoner set up for locales order and linorder.
2007-09-18 ballarin 2007-09-18 Simplified proofs due to transitivity reasoner setup.
2007-09-18 ballarin 2007-09-18 Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
2007-09-18 ballarin 2007-09-18 Morphisms applied in global interpretations behave correctly on types and terms.
2007-09-18 ballarin 2007-09-18 New function inst_morphism'.
2007-09-18 ballarin 2007-09-18 Transitivity reasoner set up for locales.
2007-09-18 wenzelm 2007-09-18 removed dead/unmaintained code;
2007-09-18 wenzelm 2007-09-18 simplified PrintMode interfaces;
2007-09-18 wenzelm 2007-09-18 moved Tools/integer.ML to Pure/General/integer.ML;
2007-09-18 paulson 2007-09-18 metis now available in PreList
2007-09-18 wenzelm 2007-09-18 reactivated tests in smlnj;
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-09-18 haftmann 2007-09-18 (reverted to previous version)
2007-09-18 haftmann 2007-09-18 updated
2007-09-18 nipkow 2007-09-18 *** empty log message ***
2007-09-18 haftmann 2007-09-18 introduced generic concepts for theory interpretators
2007-09-18 haftmann 2007-09-18 separated code for inductive sequences from inductive_codegen.ML
2007-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-09-18 haftmann 2007-09-18 renamed constructor RealC to Ratreal
2007-09-18 haftmann 2007-09-18 renamed constructor RatC to Rational
2007-09-18 haftmann 2007-09-18 clarified evaluation code
2007-09-18 haftmann 2007-09-18 adjusted
2007-09-18 haftmann 2007-09-18 clarified remark
2007-09-18 haftmann 2007-09-18 added script checking for consistency of ML file header
2007-09-18 nipkow 2007-09-18 sorting
2007-09-18 nipkow 2007-09-18 sorting
2007-09-18 nipkow 2007-09-18 Added function package to PreList Added sorted/sort to List Moved qsort from ex to Library
2007-09-17 wenzelm 2007-09-17 change print_mode: CRITICAL;
2007-09-17 wenzelm 2007-09-17 added print_mode_value (CRITICAL);
2007-09-17 wenzelm 2007-09-17 avoid direct access to print_mode;