2007-10-10 paulson 2007-10-10 getting rid of type typ_var
2007-10-09 wenzelm 2007-10-09 tuned;
2007-10-09 wenzelm 2007-10-09 class: print result is for locale;
2007-10-09 paulson 2007-10-09 context-based treatment of generalization; also handling TFrees in axiom clauses
2007-10-09 wenzelm 2007-10-09 TheoryTarget.init_cmd;
2007-10-09 wenzelm 2007-10-09 removed LocalTheory.defs/target_morphism operations; moved target_morphism to local_theory.ML; renamed init_i to init, and init to init_cmd; tuned;
2007-10-09 wenzelm 2007-10-09 renamed AxClass.get_definition to AxClass.get_info (again); simplified goal setup using Proof.theorem_i;
2007-10-09 wenzelm 2007-10-09 removed LocalTheory.defs/target_morphism operations; added target_morphism (from theory_target.ML);
2007-10-09 wenzelm 2007-10-09 AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-09 wenzelm 2007-10-09 removed LocalTheory.defs/target_morphism operations;
2007-10-09 wenzelm 2007-10-09 renamed AxClass.get_definition to AxClass.get_info (again); tuned intro_classes_tac;
2007-10-09 wenzelm 2007-10-09 renamed AxClass.get_definition to AxClass.get_info (again); AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-09 wenzelm 2007-10-09 renamed AxClass.get_definition to AxClass.get_info (again);
2007-10-09 wenzelm 2007-10-09 Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-09 wenzelm 2007-10-09 AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-09 wenzelm 2007-10-09 removed LocalTheory.defs, use plain LocalTheory.def;
2007-10-09 wenzelm 2007-10-09 tuned;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations; added uncheck/unparse_classrel/arity (from sign.ML); tuned;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations; proper installation of unparsers and term_uncheck (contract_abbrevs); removed obsolete pretty/string_of_term/typ/sort/classrel/arity (cf. structure Syntax); tuned;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations; existing pretty_term = Syntax.pretty_term o ProofContext.init etc.; removed pretty_classrel/arity (cf. Syntax/syntax.ML);
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-08 haftmann 2007-10-08 updated keywords
2007-10-08 haftmann 2007-10-08 moved translation kernel to CodeThingol
2007-10-08 haftmann 2007-10-08 tuned
2007-10-08 haftmann 2007-10-08 simplified evaluation
2007-10-08 haftmann 2007-10-08 integrated FixedPoint into Inductive
2007-10-08 haftmann 2007-10-08 added proper subclass concept; improved class target
2007-10-08 chaieb 2007-10-08 fixed bug in grobner_ideal
2007-10-08 wenzelm 2007-10-08 tuned generated comment;
2007-10-08 wenzelm 2007-10-08 primitive add_def: strip sorts in axiom;
2007-10-08 wenzelm 2007-10-08 avoid polymorphic equality;
2007-10-08 wenzelm 2007-10-08 maintain typargs for abbrevs as well;
2007-10-08 wenzelm 2007-10-08 Codegen.is_instance: raw match, ignore sort constraints; replaced get_axiom by authentic get_axiom_i;
2007-10-08 wenzelm 2007-10-08 Codegen.is_instance: raw match, ignore sort constraints;
2007-10-08 wenzelm 2007-10-08 turned keywords invariant/freshness_context into reserved indentifiers;
2007-10-08 wenzelm 2007-10-08 tuned generated comment;
2007-10-08 wenzelm 2007-10-08 updated;
2007-10-08 wenzelm 2007-10-08 moved HOL-Nominal keywords into default collection (isar-keywords.el);
2007-10-08 berghofe 2007-10-08 list_codegen and char_codegen now call invoke_tycodegen to ensure that gen_... and term_of_... functions are generated as well.
2007-10-08 haftmann 2007-10-08 added first version of user-space type system for class target
2007-10-08 haftmann 2007-10-08 clarified
2007-10-08 urbanc 2007-10-08 Isar-fied many proofs
2007-10-08 urbanc 2007-10-08 changed VC-Compatible to VC_Compatible
2007-10-08 urbanc 2007-10-08 changed file name
2007-10-08 urbanc 2007-10-08 added the two new examples from Nominal to the build process
2007-10-08 urbanc 2007-10-08 added two new example files
2007-10-07 wenzelm 2007-10-07 modernized specifications;
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-10-07 wenzelm 2007-10-07 replaced some 'translations' by 'abbreviation';
2007-10-07 wenzelm 2007-10-07 * Basic Isabelle mode for jEdit.
2007-10-07 wenzelm 2007-10-07 tuned generated comment;
2007-10-07 wenzelm 2007-10-07 tuned;
2007-10-07 wenzelm 2007-10-07 Basic Isabelle mode for jEdit -- http://www.jedit.org/
2007-10-07 wenzelm 2007-10-07 isabelle mode for jEdit;
2007-10-07 wenzelm 2007-10-07 added target tool specification; added jEdit output;
2007-10-07 wenzelm 2007-10-07 added target tool specification; no special treatment of Pure session;
2007-10-07 wenzelm 2007-10-07 emacs vs. jedit;
2007-10-06 wenzelm 2007-10-06 some updates;
2007-10-06 wenzelm 2007-10-06 removed obsolete write_keywords;
2007-10-06 wenzelm 2007-10-06 Dummy session with outer syntax keyword initialization.