| Wed, 13 Aug 2008 20:57:26 +0200 |
wenzelm |
simplified markup commands -- removed obsolete Present.results, always check text;
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 20:27:40 +0200 |
wenzelm |
removed obsolete apply_theorems(_i);
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:40 +0200 |
haftmann |
PureThy: dropped note_thmss_qualified, dropped _i suffix
|
file |
diff |
annotate
|
| Tue, 15 Jul 2008 22:37:58 +0200 |
wenzelm |
renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 19:20:57 +0200 |
haftmann |
dropped junk
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 17:51:41 +0200 |
wenzelm |
renamed theory to init_theory, removed obsolete kill argument;
|
file |
diff |
annotate
|
| Mon, 14 Jul 2008 11:19:39 +0200 |
wenzelm |
removed obsolete history commands;
|
file |
diff |
annotate
|
| Tue, 08 Jul 2008 17:52:24 +0200 |
wenzelm |
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
|
file |
diff |
annotate
|
| Wed, 02 Jul 2008 16:40:17 +0200 |
wenzelm |
Toplevel.init_theory: pass name explicitly;
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:36 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:06 +0200 |
wenzelm |
moved ProofContext.pretty_proof to ProofSyntax.pretty_proof;
|
file |
diff |
annotate
|
| Sat, 14 Jun 2008 17:26:07 +0200 |
wenzelm |
removed exotic 'token_translation' command;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 16:30:50 +0200 |
wenzelm |
token translations: context dependent, result Pretty.T;
|
file |
diff |
annotate
|
| Wed, 16 Apr 2008 21:53:02 +0200 |
wenzelm |
PureThy.defined_fact;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 18:49:26 +0200 |
wenzelm |
added hide_names command (formerly Sign.hide_names), support fact name space;
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:35 +0200 |
wenzelm |
rep_cterm/rep_thm: no longer dereference theory_ref;
|
file |
diff |
annotate
|
| Thu, 10 Apr 2008 13:24:13 +0200 |
wenzelm |
Context.set_thread_data: non-critical;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 22:56:00 +0100 |
wenzelm |
simplified print_simpset;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:11 +0100 |
wenzelm |
removed obsolete use_XXX;
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 00:02:54 +0100 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 14:41:10 +0100 |
wenzelm |
renamed ML_Context.the_context to ML_Context.the_global_context;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:07 +0100 |
wenzelm |
adapted to Context.thread_data interface;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 20:14:36 +0100 |
wenzelm |
removed obsolete use_thy (cf. isar_syn.ML);
|
file |
diff |
annotate
|
| Mon, 24 Mar 2008 23:34:24 +0100 |
wenzelm |
ML runtime compilation: pass position, tuned signature;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2008 18:59:22 +0100 |
wenzelm |
unused_thms: print via official context (ProofContext.pretty_fact),
|
file |
diff |
annotate
|
| Thu, 28 Feb 2008 17:33:35 +0100 |
berghofe |
Added unused_thms command.
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 14:20:51 +0100 |
wenzelm |
tuned names;
|
file |
diff |
annotate
|
| Sun, 10 Feb 2008 20:49:47 +0100 |
wenzelm |
tuned default position;
|
file |
diff |
annotate
|
| Thu, 24 Jan 2008 23:51:17 +0100 |
wenzelm |
removed unused Toplevel.properties;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 22:25:13 +0100 |
wenzelm |
nested_command: simplified properties vs. position -- the latter also includes id now;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 23:00:52 +0100 |
wenzelm |
added nested_command (with explicit position argument via properties);
|
file |
diff |
annotate
|
| Wed, 07 Nov 2007 22:20:09 +0100 |
wenzelm |
Syntax.read_typ;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2007 12:25:04 +0200 |
ballarin |
Simplified interface for printing of interpretations.
|
file |
diff |
annotate
|
| Sat, 08 Sep 2007 19:58:36 +0200 |
wenzelm |
thy_deps: ThyInfo.thy_ord, improved dir/unfold entry;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2007 15:46:59 +0200 |
wenzelm |
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 23:10:46 +0200 |
wenzelm |
removed obsolete touch_all_thys;
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 20:19:50 +0200 |
wenzelm |
theory loader: removed obsolete update_thy (coincides with use_thy);
|
file |
diff |
annotate
|
| Wed, 01 Aug 2007 16:55:43 +0200 |
wenzelm |
renamed 'print_options' to 'print_configs';
|
file |
diff |
annotate
|
| Mon, 30 Jul 2007 11:12:28 +0200 |
wenzelm |
marked some CRITICAL sections;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 22:01:06 +0200 |
wenzelm |
type Morphism.declaration;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 20:40:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2007 21:55:19 +0200 |
wenzelm |
renamed Config to ConfigOption;
|
file |
diff |
annotate
|
| Wed, 25 Jul 2007 22:20:51 +0200 |
wenzelm |
added command 'print_options';
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 16:45:03 +0200 |
wenzelm |
PrintMode.with_modes;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 13:53:47 +0200 |
wenzelm |
simplified ThyInfo.begin_theory;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 23:18:51 +0200 |
wenzelm |
removed obsolete use/update_thy_only;
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 11:44:20 +0200 |
wenzelm |
type output = string indicates raw system output;
|
file |
diff |
annotate
|
| Tue, 26 Jun 2007 00:35:14 +0200 |
wenzelm |
fixed undo: try undos_proof first!
|
file |
diff |
annotate
|
| Tue, 08 May 2007 17:40:20 +0200 |
wenzelm |
tuned ProofDisplay.pretty_full_theory;
|
file |
diff |
annotate
|
| Thu, 05 Apr 2007 00:30:32 +0200 |
wenzelm |
thy_deps: sort Context.thy_ord;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:42 +0200 |
wenzelm |
simplified thy_deps using Theory.ancestors_of (in order of creation);
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:19 +0200 |
wenzelm |
avoid clash with Alice keywords;
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:42 +0100 |
haftmann |
added theory dependency graph
|
file |
diff |
annotate
|
| Tue, 20 Feb 2007 00:14:33 +0100 |
kleing |
Remove duplicates from printed theorems in find_theorems
|
file |
diff |
annotate
|
| Sun, 04 Feb 2007 22:02:19 +0100 |
wenzelm |
tuned oracle interface;
|
file |
diff |
annotate
|