| Mon, 23 Jul 2007 14:06:12 +0200 |
wenzelm |
marked some CRITICAL sections (for multithreading);
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:02:04 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
| Sat, 02 Jun 2007 18:05:33 +0200 |
wenzelm |
moved specific target/local_abbrev to theory_target.ML;
|
file |
diff |
annotate
|
| Tue, 08 May 2007 17:40:22 +0200 |
wenzelm |
simplified pretty_thm(_legacy);
|
file |
diff |
annotate
|
| Tue, 08 May 2007 15:01:33 +0200 |
wenzelm |
legacy_intern_skolem: legacy_feature;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2007 20:44:12 +0200 |
wenzelm |
sane version of read_termTs (proper freeze);
|
file |
diff |
annotate
|
| Sat, 21 Apr 2007 11:07:42 +0200 |
wenzelm |
added decode_term (belongs to Syntax module);
|
file |
diff |
annotate
|
| Wed, 18 Apr 2007 21:30:14 +0200 |
wenzelm |
simplified ProofContext.infer_types(_pats);
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 23:25:55 +0200 |
wenzelm |
replaced read_term_legacy by read_prop_legacy;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:32:01 +0200 |
wenzelm |
proper interface infer_types(_pat);
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:05 +0200 |
wenzelm |
Term.string_of_vname;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 00:46:20 +0200 |
wenzelm |
added Morphism.transform/form (generic non-sense);
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 00:11:20 +0200 |
wenzelm |
renamed Output.has_mode to print_mode_active;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 20:14:52 +0100 |
wenzelm |
added theorems_of;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2007 08:39:25 +0100 |
haftmann |
add_path for naming in proof contexts
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 15:47:34 +0100 |
wenzelm |
target_abbrev: internal mode for abbrevs;
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 14:52:30 +0100 |
wenzelm |
local_abbrev: proper fix/declare of local entities;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 21:25:13 +0100 |
wenzelm |
add_abbrev: removed Assumption.add_assms (danger of inconsistent naming);
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 20:49:30 +0100 |
wenzelm |
notation: Term.equiv_types;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2006 21:39:26 +0100 |
wenzelm |
advanced translation functions: Proof.context;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 17:37:55 +0100 |
wenzelm |
removed junk;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 15:30:43 +0100 |
wenzelm |
added target_notation/abbrev;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:48 +0100 |
wenzelm |
added read/pretty_term_abbrev, print_abbrevs;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 21:08:48 +0100 |
wenzelm |
simplified add_abbrev -- single argument;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 17:58:46 +0100 |
wenzelm |
simplified add_abbrevs: no mixfix;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 00:42:04 +0100 |
wenzelm |
reorganized structure Goal vs. Tactic;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:18:58 +0100 |
wenzelm |
add_abbrevs: moved common parts to consts.ML;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:52 +0100 |
wenzelm |
add_notation: permissive about undeclared consts;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 01:17:32 +0100 |
wenzelm |
more careful indexing of local facts;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 00:29:13 +0100 |
wenzelm |
note_thmss: added kind tag and non-official name;
|
file |
diff |
annotate
|
| Fri, 01 Dec 2006 17:22:32 +0100 |
haftmann |
made SML/NJ happy
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 16:48:41 +0100 |
wenzelm |
note_thmss: refrain from closing the derivation here;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:36 +0100 |
wenzelm |
removed obsolete (export_)standard;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 23:33:09 +0100 |
wenzelm |
*** bad commit -- reverted to previous version ***
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 23:28:13 +0100 |
wenzelm |
removed export_standard_morphism;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:45:00 +0100 |
wenzelm |
removed export_standard_morphism;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:16 +0100 |
wenzelm |
removed export_standard_morphism;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2006 00:35:26 +0100 |
wenzelm |
simplified '?' operator;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:27 +0100 |
wenzelm |
added export_(standard_)morphism;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:41 +0100 |
wenzelm |
added stmt mode, which affects naming/indexing of local facts;
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 22:17:01 +0100 |
wenzelm |
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 21:44:27 +0100 |
wenzelm |
abbrevs: return result;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 11:46:50 +0100 |
wenzelm |
replaced const_syntax by notation, which operates on terms;
|
file |
diff |
annotate
|
| Sun, 05 Nov 2006 21:44:37 +0100 |
wenzelm |
added const_syntax_name;
|
file |
diff |
annotate
|
| Fri, 29 Sep 2006 22:47:01 +0200 |
wenzelm |
Syntax.mode;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:40 +0200 |
wenzelm |
added standard;
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:12:47 +0200 |
wenzelm |
pretty_thm: graceful treatment of ProtoPure.thy;
|
file |
diff |
annotate
|
| Wed, 09 Aug 2006 00:12:39 +0200 |
wenzelm |
renamed map_theory to theory;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 17:30:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:27:04 +0200 |
wenzelm |
normalized Proof.context/method type aliases;
|
file |
diff |
annotate
|
| 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
|