isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

Fri, 19 Jan 2007 22:14:23 +0100 tuned;

changeset

wenzelm [Fri, 19 Jan 2007 22:14:23 +0100] rev 22125

tuned;

Fri, 19 Jan 2007 22:10:35 +0100 renamed Isar/isar_output.ML to Thy/thy_output.ML;

changeset

wenzelm [Fri, 19 Jan 2007 22:10:35 +0100] rev 22124

renamed Isar/isar_output.ML to Thy/thy_output.ML; tuned messages; Antiquote.scan_arguments (moved from here); moved ML context stuff to from Context to ML_Context;

Fri, 19 Jan 2007 22:08:32 +0100 moved ML context stuff to from Context to ML_Context;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:32 +0100] rev 22123

moved ML context stuff to from Context to ML_Context; theorem(s): same kind;

Fri, 19 Jan 2007 22:08:31 +0100 results: proper context;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:31 +0100] rev 22122

results: proper context;

Fri, 19 Jan 2007 22:08:30 +0100 tuned Scan.extend_lexicon;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:30 +0100] rev 22121

tuned Scan.extend_lexicon;

Fri, 19 Jan 2007 22:08:29 +0100 renamed IsarOutput to ThyOutput;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:29 +0100] rev 22120

renamed IsarOutput to ThyOutput; tuned Scan.extend_lexicon; moved ML context stuff to from Context to ML_Context;

Fri, 19 Jan 2007 22:08:28 +0100 moved parts to spec_parse.ML;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:28 +0100] rev 22119

moved parts to spec_parse.ML; tuned signature -- more exports;

Fri, 19 Jan 2007 22:08:27 +0100 removed obsolete Method;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:27 +0100] rev 22118

removed obsolete Method; added parse (from outer_parse.ML); moved ML context stuff to from Context to ML_Context; tactic: no need to rebind thm/thms;

Fri, 19 Jan 2007 22:08:26 +0100 renamed IsarOutput to ThyOutput;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:26 +0100] rev 22117

renamed IsarOutput to ThyOutput; moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;

Fri, 19 Jan 2007 22:08:25 +0100 added various ML setup functions (from sign.ML, pure_thy.ML);

changeset

wenzelm [Fri, 19 Jan 2007 22:08:25 +0100] rev 22116

added various ML setup functions (from sign.ML, pure_thy.ML);

Fri, 19 Jan 2007 22:08:24 +0100 removed obsolete Attribute;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:24 +0100] rev 22115

removed obsolete Attribute;

Fri, 19 Jan 2007 22:08:23 +0100 tuned signature;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:23 +0100] rev 22114

tuned signature; added scan_arguments;

Fri, 19 Jan 2007 22:08:22 +0100 renamed Isar/isar_output.ML to Thy/thy_output.ML;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:22 +0100] rev 22113

renamed Isar/isar_output.ML to Thy/thy_output.ML; renamed Isar/term_style.ML to Thy/term_style.ML; renamed Isar/thy_header.ML to Thy/thy_header.ML; added Isar/spec_parse.ML; added Thy/ml_context.ML; load outer_parse.ML early, moved later parts to spec_parse.ML; tuned order;

Fri, 19 Jan 2007 22:08:21 +0100 tuned signature of extend_lexicon;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:21 +0100] rev 22112

tuned signature of extend_lexicon;

Fri, 19 Jan 2007 22:08:20 +0100 moved ML translation interfaces to isar_cmd.ML;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:20 +0100] rev 22111

moved ML translation interfaces to isar_cmd.ML;

Fri, 19 Jan 2007 22:08:19 +0100 moved thm/thms to ml_context.ML;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:19 +0100] rev 22110

moved thm/thms to ml_context.ML; moved generic_setup, add_oracle to isar_cmd.ML;

Fri, 19 Jan 2007 22:08:18 +0100 moved inst from drule.ML to old_goals.ML;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:18 +0100] rev 22109

moved inst from drule.ML to old_goals.ML;

Fri, 19 Jan 2007 22:08:16 +0100 tuned order;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:16 +0100] rev 22108

tuned order;

Fri, 19 Jan 2007 22:08:15 +0100 renamed Isar/term_style.ML to Thy/term_style.ML;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:15 +0100] rev 22107

renamed Isar/term_style.ML to Thy/term_style.ML;

Fri, 19 Jan 2007 22:08:14 +0100 renamed Isar/thy_header.ML to Thy/thy_header.ML;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:14 +0100] rev 22106

renamed Isar/thy_header.ML to Thy/thy_header.ML;

Fri, 19 Jan 2007 22:08:13 +0100 ML context and antiquotations (material from context.ML);

changeset

wenzelm [Fri, 19 Jan 2007 22:08:13 +0100] rev 22105

ML context and antiquotations (material from context.ML); added thm/thms (from pure_thy.ML); added support for ML antiquotations;

Fri, 19 Jan 2007 22:08:12 +0100 Parsers for complex specifications (material from outer_parse.ML);

changeset

wenzelm [Fri, 19 Jan 2007 22:08:12 +0100] rev 22104

Parsers for complex specifications (material from outer_parse.ML);

Fri, 19 Jan 2007 22:08:11 +0100 renamed Isar/isar_output.ML to Thy/thy_output.ML;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:11 +0100] rev 22103

renamed Isar/isar_output.ML to Thy/thy_output.ML; renamed Isar/term_style.ML to Thy/term_style.ML; renamed Isar/thy_header.ML to Thy/thy_header.ML; added Isar/spec_parse.ML; added Thy/ml_context.ML;

Fri, 19 Jan 2007 22:08:10 +0100 moved parts of OuterParse to SpecParse;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:10 +0100] rev 22102

moved parts of OuterParse to SpecParse; renamed OuterParse locale_target to target;

Fri, 19 Jan 2007 22:08:08 +0100 moved parts of OuterParse to SpecParse;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:08 +0100] rev 22101

moved parts of OuterParse to SpecParse;

Fri, 19 Jan 2007 22:08:07 +0100 HOL-Lambda: usedir -m no_brackets;

changeset

wenzelm [Fri, 19 Jan 2007 22:08:07 +0100] rev 22100

HOL-Lambda: usedir -m no_brackets;