2006-11-26 wenzelm 2006-11-26 Binder: syntax const is determined by binder_name, not its syntax;
2006-11-26 wenzelm 2006-11-26 simplified consts: no auxiliary params, sane mixfix syntax; declarations: proper morphisms; added target_morphism/name;
2006-11-26 wenzelm 2006-11-26 abbrevs: no result; Element.map_ctxt_attrib;
2006-11-26 wenzelm 2006-11-26 added export_(standard_)morphism;
2006-11-26 wenzelm 2006-11-26 Element.map_ctxt_attrib;
2006-11-26 wenzelm 2006-11-26 abbrevs: no result; added target_morphism/name; simplified theory prefix (no option); proper morphing of abbrevs/notation;
2006-11-26 wenzelm 2006-11-26 added map_ctxt_attrib;
2006-11-26 wenzelm 2006-11-26 abbrevs: no result;
2006-11-26 wenzelm 2006-11-26 added morh_result, the_inductive, add_inductive_global; removed get_inductive; more careful treatment of result naming/morphing;
2006-11-26 wenzelm 2006-11-26 InductivePackage.add_inductive_global;
2006-11-26 wenzelm 2006-11-26 updated (binder) syntax/notation;
2006-11-24 wenzelm 2006-11-24 tuned morphisms;
2006-11-24 wenzelm 2006-11-24 added export_morphism; ProofContext.init;
2006-11-24 wenzelm 2006-11-24 simultaneous fact morphism;
2006-11-24 wenzelm 2006-11-24 added type_map;
2006-11-24 wenzelm 2006-11-24 added cterm_rule;
2006-11-24 wenzelm 2006-11-24 fake predeclaration of structure ProofContext;
2006-11-24 wenzelm 2006-11-24 added export_morphism;
2006-11-24 wenzelm 2006-11-24 ProofContext.init;
2006-11-24 aspinall 2006-11-24 Comment: see RFC 2396 for relative URI syntax.
2006-11-24 aspinall 2006-11-24 Send full paths in PGIP version of file loaded/retracted messages
2006-11-24 paulson 2006-11-24 Conversion of "equal" to "=" for TSTP format; big tidy-up
2006-11-24 krauss 2006-11-24 Lemma "fundef_default_value" uses predicate instead of set.
2006-11-24 krauss 2006-11-24 The function package declares the [code] attribute automatically again.
2006-11-24 krauss 2006-11-24 exported mk_base_funs for use by size-change tools
2006-11-24 paulson 2006-11-24 ATP linkup now generates "new TPTP" rather than "old TPTP"
2006-11-23 wenzelm 2006-11-23 more careful declaration of "inducts";
2006-11-23 wenzelm 2006-11-23 tuned;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic; tuned;
2006-11-23 wenzelm 2006-11-23 tuned proofs;
2006-11-23 aspinall 2006-11-23 Accept URLs of form file:/home... also.
2006-11-23 wenzelm 2006-11-23 prefer antiquotations over LaTeX macros;
2006-11-23 wenzelm 2006-11-23 updated;
2006-11-23 wenzelm 2006-11-23 renamed Args.Name to Args.Text;
2006-11-23 wenzelm 2006-11-23 uniform interface for type_syntax/term_syntax/declaration, dependent on morphism; tuned some morphisms;
2006-11-23 wenzelm 2006-11-23 uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
2006-11-23 wenzelm 2006-11-23 Morphism.thm_morphism;
2006-11-23 wenzelm 2006-11-23 renamed Name value to Text, which is *not* a name in terms of morphisms;
2006-11-23 wenzelm 2006-11-23 removed obsolete alphanum;
2006-11-23 wenzelm 2006-11-23 str_of_char: improved output of non-printables;
2006-11-23 wenzelm 2006-11-23 added head_name_of;
2006-11-23 wenzelm 2006-11-23 added name/var/typ/term/thm_morphism; removed transfer;
2006-11-23 wenzelm 2006-11-23 declarations: pass morphism (dummy);
2006-11-23 wenzelm 2006-11-23 added ISABELLE_IDENTIFIER; removed THIS_IS_ISABELLE_BUILD magic;
2006-11-23 wenzelm 2006-11-23 ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;
2006-11-23 urbanc 2006-11-23 fixed some typos
2006-11-23 urbanc 2006-11-23 tuned the proof of the strong induction principle
2006-11-23 webertj 2006-11-23 typo in comment fixed
2006-11-23 aspinall 2006-11-23 Add retractfile to supported pgip commands
2006-11-23 aspinall 2006-11-23 PGIP: add retractfile. Be stricter in file open/close protocol.
2006-11-23 wenzelm 2006-11-23 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
2006-11-23 wenzelm 2006-11-23 moved ML identifiers to structure ML_Syntax;
2006-11-23 wenzelm 2006-11-23 added morph_ctxt, morph_witness; removed ctxt/witness in favour of general morphisms;
2006-11-23 wenzelm 2006-11-23 replaced map_values by morph_values;
2006-11-23 wenzelm 2006-11-23 moved string_of_pair/list/option to structure ML_Syntax;
2006-11-23 wenzelm 2006-11-23 moved ML syntax operations to structure ML_Syntax;
2006-11-23 wenzelm 2006-11-23 Basic ML syntax operations.
2006-11-23 wenzelm 2006-11-23 Abstract morphisms on formal entities.
2006-11-23 wenzelm 2006-11-23 added morphism.ML, General/ml_syntax.ML;