wenzelm [Fri, 17 Jun 2005 18:33:25 +0200] rev 16440
Context.theory_name;
tuned;
wenzelm [Fri, 17 Jun 2005 18:33:24 +0200] rev 16439
added serial numbers;
wenzelm [Fri, 17 Jun 2005 18:33:23 +0200] rev 16438
removed obsolete pretty printers for Theory.theory, Sign.sg;
added pretty printer for Context.theory (long form of output);
wenzelm [Fri, 17 Jun 2005 18:33:22 +0200] rev 16437
removed pretty_theory, pprint_theory (see context.ML or thy_info.ML);
removed obsolete pretty_name_space;
accomodate identification of type Sign.sg and theory;
wenzelm [Fri, 17 Jun 2005 18:33:21 +0200] rev 16436
added type theory: generic theory contexts with unique identity,
arbitrarily typed data, linear and graph development -- a complete
rewrite of code that used to be spread over in sign.ML, theory.ML,
theory_data.ML, pure_thy.ML;
wenzelm [Fri, 17 Jun 2005 18:33:20 +0200] rev 16435
removed Pure/theory_data.ML;
wenzelm [Fri, 17 Jun 2005 18:33:19 +0200] rev 16434
added Id;
wenzelm [Fri, 17 Jun 2005 18:33:18 +0200] rev 16433
Theory.merge;
wenzelm [Fri, 17 Jun 2005 18:33:17 +0200] rev 16432
accomodate change of TheoryDataFun;
accomodate identification of type Sign.sg and theory;
Context.theory_name;
wenzelm [Fri, 17 Jun 2005 18:33:16 +0200] rev 16431
Context.theory_name;