2007-09-25 wenzelm 2007-09-25 simplified interpretation setup;
2007-09-25 haftmann 2007-09-25 size hook
2007-09-25 wenzelm 2007-09-25 removed redundant global_parse operations; renamed global_XXX to XXX_global;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read; no export of read/cert_axm;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-09-25 wenzelm 2007-09-25 * Pure/Syntax: generic interfaces for parsing and type checking; tuned;
2007-09-25 ballarin 2007-09-25 Simplified proof due to improved integration of order_tac and simp.
2007-09-25 ballarin 2007-09-25 Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
2007-09-25 haftmann 2007-09-25 dropped
2007-09-25 haftmann 2007-09-25 ML monad support
2007-09-25 haftmann 2007-09-25 no cleverness for instance parameters
2007-09-25 haftmann 2007-09-25 added conversions for natural numbers
2007-09-25 haftmann 2007-09-25 datatype interpretators for size and datatype_realizer
2007-09-25 nipkow 2007-09-25 hide successor
2007-09-24 nipkow 2007-09-24 fixed haftmann bug
2007-09-24 wenzelm 2007-09-24 added @{theory_ref};
2007-09-24 wenzelm 2007-09-24 added @{type_name};
2007-09-24 wenzelm 2007-09-24 added polymorphic_types;
2007-09-24 wenzelm 2007-09-24 eliminated ProofContext.read_termTs;
2007-09-24 wenzelm 2007-09-24 more ML antiqs;
2007-09-24 nipkow 2007-09-24 localized { .. } (but only a few thms)
2007-09-24 wenzelm 2007-09-24 renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;
2007-09-24 wenzelm 2007-09-24 renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML; replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
2007-09-24 wenzelm 2007-09-24 replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
2007-09-23 wenzelm 2007-09-23 removed dead code; tuned;
2007-09-23 wenzelm 2007-09-23 made smlnj happy;
2007-09-23 wenzelm 2007-09-23 tuned @{cpat};
2007-09-23 wenzelm 2007-09-23 added read_term_pattern/schematic/abbrev; prepare_patterns: Variable.polymorphic; removed obsolete cert/pats versions;
2007-09-23 wenzelm 2007-09-23 ProofContext.read_term_pattern;
2007-09-23 wenzelm 2007-09-23 constrain: canonical argument order; removed obsolete logicT;
2007-09-23 wenzelm 2007-09-23 tuned;
2007-09-23 wenzelm 2007-09-23 TypeInfer.constrain: canonical argument order;
2007-09-23 wenzelm 2007-09-23 tuned ML setup;
2007-09-23 urbanc 2007-09-23 tuned one proof so to not run in a loop with the new atom-representation
2007-09-23 urbanc 2007-09-23 changed the representation of atoms to datatypes over nats
2007-09-22 wenzelm 2007-09-22 ProofContext.mode_abbrev;
2007-09-22 wenzelm 2007-09-22 removed obsolete set_expand_abbrevs (superceded by mode_abbrev); pretty_term_abbrev: silently ignore ill-typed term; gen_bind: set_mode only locally;
2007-09-22 wenzelm 2007-09-22 certify': proper do_expand argument (which observes force_expand consts) instead of home-grown normalize;
2007-09-22 wenzelm 2007-09-22 certify: do_expand as explicit argument, actually certify type of abstractions; tuned signature; tuned;
2007-09-21 wenzelm 2007-09-21 tuned;
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;