wenzelm [Wed, 11 Oct 2006 00:31:38 +0200] rev 20965
add_locale(_i): return actual result context;
cert_facts: allow qualified names;
wenzelm [Wed, 11 Oct 2006 00:27:39 +0200] rev 20964
class(_i): mimic Locale.add_locale(_i);
'class': begin_local_theory;
wenzelm [Wed, 11 Oct 2006 00:27:38 +0200] rev 20963
added type global_theory -- theory or local_theory;
added begin/exit_local_theory;
removed theory_context;
renamed body_context_node to presentation_context;
removed copy (checkpoint twice instead -- avoids unrelated theories);
wenzelm [Wed, 11 Oct 2006 00:27:37 +0200] rev 20962
added begin;
wenzelm [Wed, 11 Oct 2006 00:27:35 +0200] rev 20961
added opt_begin;
wenzelm [Wed, 11 Oct 2006 00:27:34 +0200] rev 20960
added raw_theory(_result);
tuned;
wenzelm [Wed, 11 Oct 2006 00:27:32 +0200] rev 20959
Toplevel.end_proof;
wenzelm [Wed, 11 Oct 2006 00:27:31 +0200] rev 20958
'end': handle local theory;
'locale': begin local theory;
wenzelm [Wed, 11 Oct 2006 00:27:30 +0200] rev 20957
undo_end/kill: handle local theory;
Toplevel: generic_theory;
wenzelm [Wed, 11 Oct 2006 00:27:29 +0200] rev 20956
Toplevel: generic_theory;