wenzelm [Tue, 13 Sep 2005 22:19:40 +0200] rev 17356
added cheating, sorry_text (from skip_proofs.ML);
added method_setup (from isar_thy.ML);
wenzelm [Tue, 13 Sep 2005 22:19:39 +0200] rev 17355
load late, after proof.ML;
added goal commands: theorem, interpretation etc.;
tuned some warnings -- single line only;
wenzelm [Tue, 13 Sep 2005 22:19:38 +0200] rev 17354
moved most material to its proper place (sign.ML, pure_thy.ML, method.ML, proof.ML, locale.ML etc.);
begin_theory: tuned interface, check uses in thy_info.ML;
wenzelm [Tue, 13 Sep 2005 22:19:37 +0200] rev 17353
cleanup parsers and interfaces;
wenzelm [Tue, 13 Sep 2005 22:19:36 +0200] rev 17352
Proof.get_thmss;
wenzelm [Tue, 13 Sep 2005 22:19:35 +0200] rev 17351
tuned;
wenzelm [Tue, 13 Sep 2005 22:19:34 +0200] rev 17350
more self-contained proof elements (material from isar_thy.ML);
tuned;
wenzelm [Tue, 13 Sep 2005 22:19:33 +0200] rev 17349
added cases, rule_contextN;
eliminated obsolete Sign.sg;
wenzelm [Tue, 13 Sep 2005 22:19:32 +0200] rev 17348
load locale.ML late (after proof.ML);
tuned module arrangement;
wenzelm [Tue, 13 Sep 2005 22:19:31 +0200] rev 17347
added maps, map_list, lift, lifts;