2006-11-24 paulson 2006-11-24 Conversion of "equal" to "=" for TSTP format; big tidy-up
2006-11-24 krauss 2006-11-24 Lemma "fundef_default_value" uses predicate instead of set.
2006-11-24 krauss 2006-11-24 The function package declares the [code] attribute automatically again.
2006-11-24 krauss 2006-11-24 exported mk_base_funs for use by size-change tools
2006-11-24 paulson 2006-11-24 ATP linkup now generates "new TPTP" rather than "old TPTP"
2006-11-23 wenzelm 2006-11-23 more careful declaration of "inducts";
2006-11-23 wenzelm 2006-11-23 tuned;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic; tuned;
2006-11-23 wenzelm 2006-11-23 tuned proofs;
2006-11-23 aspinall 2006-11-23 Accept URLs of form file:/home... also.
2006-11-23 wenzelm 2006-11-23 prefer antiquotations over LaTeX macros;
2006-11-23 wenzelm 2006-11-23 updated;
2006-11-23 wenzelm 2006-11-23 renamed Args.Name to Args.Text;
2006-11-23 wenzelm 2006-11-23 uniform interface for type_syntax/term_syntax/declaration, dependent on morphism; tuned some morphisms;
2006-11-23 wenzelm 2006-11-23 uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
2006-11-23 wenzelm 2006-11-23 Morphism.thm_morphism;
2006-11-23 wenzelm 2006-11-23 renamed Name value to Text, which is *not* a name in terms of morphisms;
2006-11-23 wenzelm 2006-11-23 removed obsolete alphanum;
2006-11-23 wenzelm 2006-11-23 str_of_char: improved output of non-printables;
2006-11-23 wenzelm 2006-11-23 added head_name_of;
2006-11-23 wenzelm 2006-11-23 added name/var/typ/term/thm_morphism; removed transfer;
2006-11-23 wenzelm 2006-11-23 declarations: pass morphism (dummy);
2006-11-23 wenzelm 2006-11-23 added ISABELLE_IDENTIFIER; removed THIS_IS_ISABELLE_BUILD magic;
2006-11-23 wenzelm 2006-11-23 ISABELLE_PATH/OUTPUT: append ISABELLE_IDENTIFIER if derived from ISABELLE_HOME_USER;
2006-11-23 urbanc 2006-11-23 fixed some typos
2006-11-23 urbanc 2006-11-23 tuned the proof of the strong induction principle
2006-11-23 webertj 2006-11-23 typo in comment fixed
2006-11-23 aspinall 2006-11-23 Add retractfile to supported pgip commands
2006-11-23 aspinall 2006-11-23 PGIP: add retractfile. Be stricter in file open/close protocol.
2006-11-23 wenzelm 2006-11-23 replaced Args.map_values/Element.map_ctxt_values by general morphism application;
2006-11-23 wenzelm 2006-11-23 moved ML identifiers to structure ML_Syntax;
2006-11-23 wenzelm 2006-11-23 added morph_ctxt, morph_witness; removed ctxt/witness in favour of general morphisms;
2006-11-23 wenzelm 2006-11-23 replaced map_values by morph_values;
2006-11-23 wenzelm 2006-11-23 moved string_of_pair/list/option to structure ML_Syntax;
2006-11-23 wenzelm 2006-11-23 moved ML syntax operations to structure ML_Syntax;
2006-11-23 wenzelm 2006-11-23 Basic ML syntax operations.
2006-11-23 wenzelm 2006-11-23 Abstract morphisms on formal entities.
2006-11-23 wenzelm 2006-11-23 added morphism.ML, General/ml_syntax.ML;
2006-11-23 wenzelm 2006-11-23 renamed string_of_pair/list/option to ML_Syntax.str_of_pair/list/option;
2006-11-23 wenzelm 2006-11-23 removed dead code;
2006-11-23 aspinall 2006-11-23 Add doccomment; rename litcomment -> doccomment
2006-11-22 wenzelm 2006-11-22 * settings: ML_IDENTIFIER includes the Isabelle version identifier;
2006-11-22 paulson 2006-11-22 Consolidation of code to "blacklist" unhelpful theorems, including record surjectivity properties
2006-11-22 wenzelm 2006-11-22 ML_IDENTIFIER includes Isabelle version;
2006-11-22 wenzelm 2006-11-22 add ISABELLE_VERSION to ML_IDENTIFIER, unless this is repository or build;
2006-11-22 wenzelm 2006-11-22 consts: ProofContext.set_stmt true -- avoids naming of local thms;
2006-11-22 wenzelm 2006-11-22 init: enter inner statement mode, which prevents local notes from being named internally;
2006-11-22 wenzelm 2006-11-22 more careful declaration of "intros" as Pure.intro;
2006-11-22 aspinall 2006-11-22 Fix to local file URI syntax. Add first part of lexicalstructure command support.
2006-11-22 haftmann 2006-11-22 completed class parameter handling in axclass.ML
2006-11-22 haftmann 2006-11-22 added Isar syntax for adding parameters to axclasses
2006-11-22 haftmann 2006-11-22 forced name prefix for class operations
2006-11-22 haftmann 2006-11-22 example tuned
2006-11-22 haftmann 2006-11-22 no explicit check for theory Nat
2006-11-22 haftmann 2006-11-22 added code lemmas
2006-11-22 haftmann 2006-11-22 does not import Hilber_Choice any longer
2006-11-22 haftmann 2006-11-22 cleanup
2006-11-22 haftmann 2006-11-22 incorporated structure HOList into HOLogic
2006-11-22 haftmann 2006-11-22 dropped eq const