2007-10-01 wenzelm 2007-10-01 Norbert Schirmer: record improvements;
2007-10-01 wenzelm 2007-10-01 preliminary material for Isabelle2007;
2007-10-01 wenzelm 2007-10-01 misc tuning and update;
2007-10-01 wenzelm 2007-10-01 misc tuning and update;
2007-10-01 wenzelm 2007-10-01 misc tuning and update;
2007-10-01 wenzelm 2007-10-01 updated year to 2007;
2007-10-01 wenzelm 2007-10-01 tuned;
2007-10-01 haftmann 2007-10-01 added some lemmas
2007-10-01 wenzelm 2007-10-01 print_state_context: local theory context, not proof context; context_position: cover Theory case as well (requires additional checkpoint);
2007-10-01 wenzelm 2007-10-01 ContextPosition.put_ctxt;
2007-10-01 wenzelm 2007-10-01 NameSelection: more interval checks;
2007-10-01 wenzelm 2007-10-01 tuned message;
2007-10-01 wenzelm 2007-10-01 turned into generic context data;
2007-10-01 wenzelm 2007-10-01 ML_setup for bind_thms;
2007-10-01 ballarin 2007-10-01 Simplified interface for printing of interpretations.
2007-10-01 ballarin 2007-10-01 unfold_locales workaround
2007-10-01 ballarin 2007-10-01 Theory/context data restructured; simplified interface for printing of interpretations.
2007-10-01 isatest 2007-10-01 fixed dir in single-logic test
2007-09-30 wenzelm 2007-09-30 llabs/sko: removed Name.internal;
2007-09-30 wenzelm 2007-09-30 avoid unnamed infixes;
2007-09-30 wenzelm 2007-09-30 avoid internal names;
2007-09-30 isatest 2007-09-30 switch notification email back on
2007-09-30 isatest 2007-09-30 fix shell quoting confusion
2007-09-30 wenzelm 2007-09-30 local_theory transactions: more careful treatment of context position;
2007-09-30 wenzelm 2007-09-30 keep context position as tags for consts/thms;
2007-09-30 wenzelm 2007-09-30 add_abbrev: tags (Markup.property list);
2007-09-30 wenzelm 2007-09-30 added internalK, property_internal;
2007-09-30 wenzelm 2007-09-30 add_consts_authentic/add_abbrev: tags (Markup.property list); tuned signature;
2007-09-30 wenzelm 2007-09-30 Markup.internalK;
2007-09-30 wenzelm 2007-09-30 print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
2007-09-30 wenzelm 2007-09-30 added properties_of;
2007-09-30 wenzelm 2007-09-30 maintain tags (Markup.property list); tuned;
2007-09-30 wenzelm 2007-09-30 skofuns/absfuns: explicit markup as internal consts;
2007-09-30 wenzelm 2007-09-30 Sign.add_consts_authentic: tags (Markup.property list);
2007-09-30 wenzelm 2007-09-30 standard_term_check: include expand_abbrevs (back again);
2007-09-29 wenzelm 2007-09-29 added unparse interfaces (still unused); add_typ/term_check: added stage and name argument; added print_checks;
2007-09-29 wenzelm 2007-09-29 removed redundant const_constraint; add_const_constraint: proper certification; prepare_dummies: avoid imperative features; term_check: separate phases, standard_infer_types passes inference parameters instead of frees/vars; Syntax.install_operations: dummy unparsers;
2007-09-29 wenzelm 2007-09-29 Sign.add_const_constraint; Syntax.add_typ/term_check: added stage and name argument;
2007-09-29 wenzelm 2007-09-29 maintain maxidx (analogous to name context); polymorhic: observe Variable.maxidx_of;
2007-09-29 wenzelm 2007-09-29 added fixate_params; type_infer: freeze_mode = NONE keeps inference parameters in result; type_infer: observe Variable.maxidx_of;
2007-09-29 wenzelm 2007-09-29 Sign.the_const_constraint;
2007-09-29 wenzelm 2007-09-29 added declare_typ_names; replace_dummy_patterns: canonical argument order;
2007-09-29 wenzelm 2007-09-29 removed obsolete external interface add_const_constraint; removed redundant const_constraint; renamed add_const_constraint_i to add_const_constraint;
2007-09-29 wenzelm 2007-09-29 Sign.add_const_constraint;
2007-09-29 wenzelm 2007-09-29 fixed metis proof (Why did it stop working?);
2007-09-29 isatest 2007-09-29 swapped machines for at-sml-dev and at-sml-dev-p
2007-09-29 isatest 2007-09-29 no proof terms for smlnj
2007-09-29 kleing 2007-09-29 add -p 2 at-sml-dev test for HOL proof terms sessions only
2007-09-29 kleing 2007-09-29 at-sml-dev session with -p 2
2007-09-29 kleing 2007-09-29 Added target for proof term sessions (those that need -p 2)
2007-09-29 kleing 2007-09-29 accept single logic and target as argument
2007-09-29 haftmann 2007-09-29 exported constraint interfaces
2007-09-29 haftmann 2007-09-29 exported intern_expr
2007-09-29 haftmann 2007-09-29 added ocaml strings
2007-09-29 haftmann 2007-09-29 further localization
2007-09-29 haftmann 2007-09-29 proper syntax during class specification
2007-09-28 berghofe 2007-09-28 prove_strong_ind now uses InductivePackage.rulify.
2007-09-28 berghofe 2007-09-28 Adapted to changes in interface of add_inductive_i.
2007-09-28 berghofe 2007-09-28 add_inductive_i now takes typ instead of typ option as argument.
2007-09-28 berghofe 2007-09-28 - add_inductive_i now takes typ instead of typ option as argument - close_rule is now applied before expanding abbreviations - rulify applies norm_hhf again