wenzelm [Thu, 23 Nov 2006 20:33:42 +0100] rev 21501
updated;
wenzelm [Thu, 23 Nov 2006 20:33:41 +0100] rev 21500
renamed Args.Name to Args.Text;
wenzelm [Thu, 23 Nov 2006 20:33:39 +0100] rev 21499
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
tuned some morphisms;
wenzelm [Thu, 23 Nov 2006 20:33:37 +0100] rev 21498
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
wenzelm [Thu, 23 Nov 2006 20:33:36 +0100] rev 21497
Morphism.thm_morphism;
wenzelm [Thu, 23 Nov 2006 20:33:34 +0100] rev 21496
renamed Name value to Text, which is *not* a name in terms of morphisms;
wenzelm [Thu, 23 Nov 2006 20:33:33 +0100] rev 21495
removed obsolete alphanum;
wenzelm [Thu, 23 Nov 2006 20:33:32 +0100] rev 21494
str_of_char: improved output of non-printables;
wenzelm [Thu, 23 Nov 2006 20:33:29 +0100] rev 21493
added head_name_of;
wenzelm [Thu, 23 Nov 2006 20:33:28 +0100] rev 21492
added name/var/typ/term/thm_morphism;
removed transfer;
wenzelm [Thu, 23 Nov 2006 20:33:25 +0100] rev 21491
declarations: pass morphism (dummy);
wenzelm [Thu, 23 Nov 2006 18:49:55 +0100] rev 21490
added ISABELLE_IDENTIFIER;
removed THIS_IS_ISABELLE_BUILD magic;
wenzelm [Thu, 23 Nov 2006 18:49:03 +0100] rev 21489
ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;
urbanc [Thu, 23 Nov 2006 17:52:48 +0100] rev 21488
fixed some typos
urbanc [Thu, 23 Nov 2006 14:11:49 +0100] rev 21487
tuned the proof of the strong induction principle
webertj [Thu, 23 Nov 2006 13:32:19 +0100] rev 21486
typo in comment fixed
aspinall [Thu, 23 Nov 2006 11:39:11 +0100] rev 21485
Add retractfile to supported pgip commands
aspinall [Thu, 23 Nov 2006 11:24:33 +0100] rev 21484
PGIP: add retractfile. Be stricter in file open/close protocol.
wenzelm [Thu, 23 Nov 2006 00:52:23 +0100] rev 21483
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
wenzelm [Thu, 23 Nov 2006 00:52:19 +0100] rev 21482
moved ML identifiers to structure ML_Syntax;
wenzelm [Thu, 23 Nov 2006 00:52:15 +0100] rev 21481
added morph_ctxt, morph_witness;
removed ctxt/witness in favour of general morphisms;
wenzelm [Thu, 23 Nov 2006 00:52:11 +0100] rev 21480
replaced map_values by morph_values;
wenzelm [Thu, 23 Nov 2006 00:52:07 +0100] rev 21479
moved string_of_pair/list/option to structure ML_Syntax;
wenzelm [Thu, 23 Nov 2006 00:52:03 +0100] rev 21478
moved ML syntax operations to structure ML_Syntax;
wenzelm [Thu, 23 Nov 2006 00:52:01 +0100] rev 21477
Basic ML syntax operations.
wenzelm [Thu, 23 Nov 2006 00:51:57 +0100] rev 21476
Abstract morphisms on formal entities.
wenzelm [Thu, 23 Nov 2006 00:51:54 +0100] rev 21475
added morphism.ML, General/ml_syntax.ML;
wenzelm [Thu, 23 Nov 2006 00:51:51 +0100] rev 21474
renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;
wenzelm [Thu, 23 Nov 2006 00:51:47 +0100] rev 21473
removed dead code;
aspinall [Thu, 23 Nov 2006 00:09:24 +0100] rev 21472
Add doccomment; rename litcomment -> doccomment