Sat, 24 May 2008 23:52:35 +0200 wenzelm inst_subst_tac: match types -- no longer assume that subst rule has exactly one type argument;
Sat, 24 May 2008 22:19:35 +0200 wenzelm updated generated file;
Sat, 24 May 2008 22:04:57 +0200 wenzelm added local_theory command wrappers;
Sat, 24 May 2008 22:04:55 +0200 wenzelm uniform treatment of target, not as config;
Sat, 24 May 2008 22:04:52 +0200 wenzelm more uniform treatment of OuterSyntax.local_theory commands;
Sat, 24 May 2008 22:04:48 +0200 wenzelm updated generated file;
Sat, 24 May 2008 22:04:46 +0200 wenzelm invisible comment;
Sat, 24 May 2008 22:04:44 +0200 wenzelm function: uniform treatment of target, not as config;
Sat, 24 May 2008 20:12:18 +0200 wenzelm added parse_document (optional unchecked header material);
Sat, 24 May 2008 20:12:17 +0200 wenzelm exported master_directory;
Sat, 24 May 2008 20:12:16 +0200 wenzelm present_excursion: setmp_thread_position during presentation;
Sat, 24 May 2008 20:05:21 +0200 wenzelm use: explicit .ML;
Sat, 24 May 2008 14:47:43 +0200 wenzelm ident: naive caching prevents potentially slow external invocations;
Sat, 24 May 2008 02:19:09 +0200 urbanc fixed improper handling of return code (pdf and ps.gz formats)
Fri, 23 May 2008 21:20:26 +0200 wenzelm add constants: set Markup.theory_nameN in tags;
Fri, 23 May 2008 21:18:47 +0200 wenzelm added theory_nameN;
Fri, 23 May 2008 17:19:24 +0200 krauss rearranged subsections
Fri, 23 May 2008 16:41:39 +0200 berghofe Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
Fri, 23 May 2008 16:37:57 +0200 berghofe Replaced Pretty.str and Pretty.string_of by specific functions that
Fri, 23 May 2008 16:10:25 +0200 haftmann temporary adjustment
Fri, 23 May 2008 16:05:13 +0200 haftmann tuned
Fri, 23 May 2008 16:05:11 +0200 haftmann more permissive preprocessor
Fri, 23 May 2008 16:05:07 +0200 haftmann explicit type schemes for functions
Fri, 23 May 2008 16:05:04 +0200 haftmann moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs
Fri, 23 May 2008 16:05:02 +0200 haftmann added code for quantifiers
Fri, 23 May 2008 16:04:59 +0200 haftmann simplified proof
Thu, 22 May 2008 16:34:41 +0200 urbanc made the naming of the induction principles consistent: weak_induct is
Wed, 21 May 2008 22:04:58 +0200 gagern use_file: added str_of_pos argument (ignored);
Wed, 21 May 2008 14:04:41 +0200 berghofe Added entry explaining incompatibilities introduced by replacing sets by predicates.
Mon, 19 May 2008 23:50:06 +0200 huffman instantiation lift :: (countable) bifinite
Mon, 19 May 2008 23:49:20 +0200 huffman use new class package for classes profinite, bifinite; remove approx class
Sun, 18 May 2008 17:04:48 +0200 wenzelm updated generated file;
Sun, 18 May 2008 17:03:26 +0200 wenzelm unparse_term: check PureThy.old_appl_syntax instead of CPure;
Sun, 18 May 2008 17:03:24 +0200 wenzelm theory Pure provides regular application syntax by default;
Sun, 18 May 2008 17:03:23 +0200 wenzelm converted to regular application syntax;
Sun, 18 May 2008 17:03:20 +0200 wenzelm eliminated theory CPure;
Sun, 18 May 2008 17:03:16 +0200 wenzelm setup PureThy.old_appl_syntax_setup -- theory Pure provides regular application syntax by default;
Sun, 18 May 2008 17:03:14 +0200 wenzelm * Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
Sun, 18 May 2008 16:19:48 +0200 urbanc proper handling of the return code for the ps-format (fixes a bug)
Sun, 18 May 2008 15:28:21 +0200 wenzelm oops -- pr_graph = Syntax.string_of_term;
Sun, 18 May 2008 15:04:48 +0200 wenzelm command 'normal_form': proper context via Variable.auto_fixes;
Sun, 18 May 2008 15:04:46 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sun, 18 May 2008 15:04:45 +0200 wenzelm Syntax.string_of_sort: proper context;
Sun, 18 May 2008 15:04:43 +0200 wenzelm pprint: proper global context via Syntax.init_pretty_global;
Sun, 18 May 2008 15:04:41 +0200 wenzelm Syntax.string_of_typ: proper context;
Sun, 18 May 2008 15:04:37 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sun, 18 May 2008 15:04:33 +0200 wenzelm removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway);
Sun, 18 May 2008 15:04:31 +0200 wenzelm renamed type decompT to decomp;
Sun, 18 May 2008 15:04:27 +0200 wenzelm Syntax.string_of_term with proper context;
Sun, 18 May 2008 15:04:24 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sun, 18 May 2008 15:04:22 +0200 wenzelm renamed type decompT to decomp;
Sun, 18 May 2008 15:04:20 +0200 wenzelm pr_matrix: proper context;
Sun, 18 May 2008 15:04:17 +0200 wenzelm guess_instance: proper context;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Sat, 17 May 2008 23:53:20 +0200 wenzelm tuned comments;
Sat, 17 May 2008 23:53:19 +0200 wenzelm tuned proofs;
Sat, 17 May 2008 23:37:11 +0200 wenzelm avoid undeclared variables in facts;
Sat, 17 May 2008 23:37:09 +0200 wenzelm avoid undeclared variables within proofs;
Sat, 17 May 2008 23:37:07 +0200 wenzelm avoid undeclared variables within proofs;
Sat, 17 May 2008 21:46:24 +0200 wenzelm tuned proof;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip