Wed, 11 Oct 2006 00:27:39 +0200 class(_i): mimic Locale.add_locale(_i);
wenzelm [Wed, 11 Oct 2006 00:27:39 +0200] rev 20964
class(_i): mimic Locale.add_locale(_i); 'class': begin_local_theory;
Wed, 11 Oct 2006 00:27:38 +0200 added type global_theory -- theory or 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);
Wed, 11 Oct 2006 00:27:37 +0200 added begin;
wenzelm [Wed, 11 Oct 2006 00:27:37 +0200] rev 20962
added begin;
Wed, 11 Oct 2006 00:27:35 +0200 added opt_begin;
wenzelm [Wed, 11 Oct 2006 00:27:35 +0200] rev 20961
added opt_begin;
Wed, 11 Oct 2006 00:27:34 +0200 added raw_theory(_result);
wenzelm [Wed, 11 Oct 2006 00:27:34 +0200] rev 20960
added raw_theory(_result); tuned;
Wed, 11 Oct 2006 00:27:32 +0200 Toplevel.end_proof;
wenzelm [Wed, 11 Oct 2006 00:27:32 +0200] rev 20959
Toplevel.end_proof;
Wed, 11 Oct 2006 00:27:31 +0200 'end': handle local theory;
wenzelm [Wed, 11 Oct 2006 00:27:31 +0200] rev 20958
'end': handle local theory; 'locale': begin local theory;
Wed, 11 Oct 2006 00:27:30 +0200 undo_end/kill: handle local theory;
wenzelm [Wed, 11 Oct 2006 00:27:30 +0200] rev 20957
undo_end/kill: handle local theory; Toplevel: generic_theory;
Wed, 11 Oct 2006 00:27:29 +0200 Toplevel: generic_theory;
wenzelm [Wed, 11 Oct 2006 00:27:29 +0200] rev 20956
Toplevel: generic_theory;
Tue, 10 Oct 2006 16:26:59 +0200 made some proof look more like the ones in Barendregt
urbanc [Tue, 10 Oct 2006 16:26:59 +0200] rev 20955
made some proof look more like the ones in Barendregt
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip