| Sat, 29 Jul 2006 00:51:36 +0200 |
wenzelm |
rename legacy_pretty_thm to pretty_thm_legacy;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 23:28:30 +0200 |
wenzelm |
replaced extern_skolem by slightly more simplistic revert_skolems;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:12 +0200 |
wenzelm |
added legacy_pretty_thm (with fall-back on ProtoPure.thy);
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 00:44:47 +0200 |
wenzelm |
moved pprint functions to Isar/proof_display.ML;
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 12:12:06 +0200 |
wenzelm |
Sign.infer_types: Name.context;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 23:00:39 +0200 |
wenzelm |
adapted Name.defaults_of;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:17:12 +0200 |
wenzelm |
adapted to more efficient Name/Variable implementation;
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:37 +0200 |
wenzelm |
Goal.prove: context;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 21:22:53 +0200 |
wenzelm |
print_lthms: include unnamed facts from index;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 19:49:59 +0200 |
wenzelm |
add_abbrevs/polymorphic: Variable.exportT_terms avoids over-generalization;
|
file |
diff |
annotate
|
| Sat, 17 Jun 2006 19:37:58 +0200 |
wenzelm |
export: simultaneous facts, refer to Variable.export;
|
file |
diff |
annotate
|
| Thu, 15 Jun 2006 23:08:54 +0200 |
wenzelm |
ProofContext: moved variable operations to struct Variable;
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 23:41:58 +0200 |
wenzelm |
tuned interfaces;
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 21:19:07 +0200 |
wenzelm |
added declare_typ;
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 21:59:27 +0200 |
wenzelm |
added import -- fixes schematic variables;
|
file |
diff |
annotate
|
| Fri, 26 May 2006 22:20:07 +0200 |
wenzelm |
removed unused extern_thm;
|
file |
diff |
annotate
|
| Wed, 17 May 2006 22:34:52 +0200 |
wenzelm |
added CONST syntax;
|
file |
diff |
annotate
|
| Wed, 17 May 2006 01:23:46 +0200 |
wenzelm |
always preserve authentic consts -- removed Syntax.mixfix_const;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:18 +0200 |
wenzelm |
export consts_of;
|
file |
diff |
annotate
|
| Sun, 07 May 2006 00:22:05 +0200 |
wenzelm |
removed 'concl is' patterns;
|
file |
diff |
annotate
|
| Tue, 02 May 2006 20:42:39 +0200 |
wenzelm |
added set_syntax_mode, restore_syntax_mode;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:00 +0200 |
wenzelm |
expand_atom: Type.raw_match;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2006 16:00:08 +0200 |
wenzelm |
export pretty_classrel/arity;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 18:51:22 +0200 |
wenzelm |
added full_name;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:28 +0200 |
wenzelm |
add_abbrevs(_i): support print mode;
|
file |
diff |
annotate
|
| Tue, 21 Mar 2006 12:18:21 +0100 |
wenzelm |
subtract (op =);
|
file |
diff |
annotate
|
| Wed, 15 Mar 2006 16:18:12 +0100 |
wenzelm |
rename_frees: treat trivial names;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 22:06:40 +0100 |
wenzelm |
added monomorphic;
|
file |
diff |
annotate
|
| Sun, 26 Feb 2006 23:01:50 +0100 |
wenzelm |
put_thms: do_index;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 18:26:03 +0100 |
wenzelm |
added put_thms_internal: local_naming, no fact index;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:12 +0100 |
wenzelm |
replaced qualified_force_prefix to sticky_prefix;
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:27 +0100 |
wenzelm |
consts: maintain thy version for efficient transfer;
|
file |
diff |
annotate
|
| Sat, 11 Feb 2006 17:17:54 +0100 |
wenzelm |
added map_theory;
|
file |
diff |
annotate
|
| Fri, 10 Feb 2006 02:22:48 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Tue, 07 Feb 2006 19:56:54 +0100 |
wenzelm |
added local consts component;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:53 +0100 |
wenzelm |
norm_term: Sign.const_expansion, Envir.expand_atom;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 11:01:28 +0100 |
haftmann |
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 12:54:24 +0100 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2006 18:19:35 +0100 |
wenzelm |
improved comments;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2006 00:39:40 +0100 |
wenzelm |
advanced translations: Context.generic;
|
file |
diff |
annotate
|
| Sun, 29 Jan 2006 19:23:51 +0100 |
wenzelm |
invent_fixes: merely enter body temporarily;
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:29:02 +0100 |
wenzelm |
moved local defs to local_defs.ML;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:15 +0100 |
wenzelm |
added invent_fixes;
|
file |
diff |
annotate
|
| Wed, 25 Jan 2006 00:21:43 +0100 |
wenzelm |
renamed export to export_standard (again!), because it includes Drule.local_standard';
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:43:33 +0100 |
wenzelm |
renamed inferred_type to inferred_param;
|
file |
diff |
annotate
|
| Sun, 22 Jan 2006 18:46:00 +0100 |
wenzelm |
added restore_body;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Mon, 16 Jan 2006 21:55:17 +0100 |
wenzelm |
case_result: drop_schematic, i.e. be permissive about illegal binds;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:13:16 +0100 |
wenzelm |
uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 23:28:00 +0100 |
wenzelm |
added infer_type, declared_type;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 12:26:35 +0100 |
wenzelm |
support nested cases;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:08 +0100 |
wenzelm |
cases: main is_proper flag;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2005 01:00:40 +0100 |
wenzelm |
sort_distinct;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2005 09:00:11 +0100 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
file |
diff |
annotate
|
| Thu, 08 Dec 2005 20:16:10 +0100 |
wenzelm |
removed Syntax.deskolem;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2005 22:54:50 +0100 |
wenzelm |
removed fixed_tr: now handled in syntax module;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 22:52:50 +0100 |
wenzelm |
match_bind(_i): return terms;
|
file |
diff |
annotate
|