2008-05-28 haftmann 2008-05-28 new serializer interface
2008-05-28 haftmann 2008-05-28 added new code_datatype example
2008-05-26 haftmann 2008-05-26 proper use of the Pretty module
2008-05-26 haftmann 2008-05-26 permissive wrt. instantiation of class operations
2008-05-26 haftmann 2008-05-26 proper lemma [source] antiquotation
2008-05-26 haftmann 2008-05-26 check for illegal merge of class parameters
2008-05-26 haftmann 2008-05-26 proper NoSubsort CLASS_ERROR
2008-05-26 haftmann 2008-05-26 tuned theorem order
2008-05-24 wenzelm 2008-05-24 inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument; misc tuning -- more cterm operations, more qualified names;
2008-05-24 wenzelm 2008-05-24 updated generated file;
2008-05-24 wenzelm 2008-05-24 added local_theory command wrappers;
2008-05-24 wenzelm 2008-05-24 uniform treatment of target, not as config;
2008-05-24 wenzelm 2008-05-24 more uniform treatment of OuterSyntax.local_theory commands;
2008-05-24 wenzelm 2008-05-24 updated generated file;
2008-05-24 wenzelm 2008-05-24 invisible comment;
2008-05-24 wenzelm 2008-05-24 function: uniform treatment of target, not as config;
2008-05-24 wenzelm 2008-05-24 added parse_document (optional unchecked header material); parse: parse_document instead of parse_element;
2008-05-24 wenzelm 2008-05-24 exported master_directory;
2008-05-24 wenzelm 2008-05-24 present_excursion: setmp_thread_position during presentation;
2008-05-24 wenzelm 2008-05-24 use: explicit .ML;
2008-05-24 wenzelm 2008-05-24 ident: naive caching prevents potentially slow external invocations; tuned comments; tuned;
2008-05-24 urbanc 2008-05-24 fixed improper handling of return code (pdf and ps.gz formats)
2008-05-23 wenzelm 2008-05-23 add constants: set Markup.theory_nameN in tags;
2008-05-23 wenzelm 2008-05-23 added theory_nameN;
2008-05-23 krauss 2008-05-23 rearranged subsections
2008-05-23 berghofe 2008-05-23 Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.
2008-05-23 berghofe 2008-05-23 Replaced Pretty.str and Pretty.string_of by specific functions that set print_mode and margin appropriately.
2008-05-23 haftmann 2008-05-23 temporary adjustment
2008-05-23 haftmann 2008-05-23 tuned
2008-05-23 haftmann 2008-05-23 more permissive preprocessor
2008-05-23 haftmann 2008-05-23 explicit type schemes for functions
2008-05-23 haftmann 2008-05-23 moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
2008-05-23 haftmann 2008-05-23 added code for quantifiers
2008-05-23 haftmann 2008-05-23 simplified proof
2008-05-22 urbanc 2008-05-22 made the naming of the induction principles consistent: weak_induct is induct and induct is strong_induct
2008-05-21 gagern 2008-05-21 use_file: added str_of_pos argument (ignored);
2008-05-21 berghofe 2008-05-21 Added entry explaining incompatibilities introduced by replacing sets by predicates.
2008-05-19 huffman 2008-05-19 instantiation lift :: (countable) bifinite
2008-05-19 huffman 2008-05-19 use new class package for classes profinite, bifinite; remove approx class
2008-05-18 wenzelm 2008-05-18 updated generated file;
2008-05-18 wenzelm 2008-05-18 unparse_term: check PureThy.old_appl_syntax instead of CPure;
2008-05-18 wenzelm 2008-05-18 theory Pure provides regular application syntax by default; added old_appl_syntax_setup for former Pure clients;
2008-05-18 wenzelm 2008-05-18 converted to regular application syntax;
2008-05-18 wenzelm 2008-05-18 eliminated theory CPure;
2008-05-18 wenzelm 2008-05-18 setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
2008-05-18 wenzelm 2008-05-18 * Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
2008-05-18 urbanc 2008-05-18 proper handling of the return code for the ps-format (fixes a bug)
2008-05-18 wenzelm 2008-05-18 oops -- pr_graph = Syntax.string_of_term; removed dead pr_matrix;
2008-05-18 wenzelm 2008-05-18 command 'normal_form': proper context via Variable.auto_fixes;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax; reordered signature;
2008-05-18 wenzelm 2008-05-18 Syntax.string_of_sort: proper context;
2008-05-18 wenzelm 2008-05-18 pprint: proper global context via Syntax.init_pretty_global;
2008-05-18 wenzelm 2008-05-18 Syntax.string_of_typ: proper context;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax; tuned message;
2008-05-18 wenzelm 2008-05-18 removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway); full_path: no link expansion here (reverted change of 1.18); ident: OS.FileSys.fullPath takes care of link expansion;
2008-05-18 wenzelm 2008-05-18 renamed type decompT to decomp; refute: proper context for trace_ex; some attempts to improve readability;
2008-05-18 wenzelm 2008-05-18 Syntax.string_of_term with proper context;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax; removed dead code;
2008-05-18 wenzelm 2008-05-18 renamed type decompT to decomp;
2008-05-18 wenzelm 2008-05-18 pr_matrix: proper context;