| 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
|
| Sun, 28 Jan 2007 23:29:16 +0100 |
wenzelm |
added simproc_setup;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:25 +0100 |
wenzelm |
added various ML setup functions (from sign.ML, pure_thy.ML);
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 13:09:35 +0100 |
wenzelm |
added 'declaration' command;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 12:33:25 +0100 |
wenzelm |
removed obsolete clear_undos_theory;
|
file |
diff |
annotate
|
| Fri, 29 Dec 2006 19:50:48 +0100 |
wenzelm |
removed obsolete init_context;
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:06 +0100 |
wenzelm |
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
|
file |
diff |
annotate
|
| Sat, 09 Dec 2006 18:05:44 +0100 |
wenzelm |
added print_abbrevs;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:48 +0100 |
wenzelm |
print_syntax etc.: plain Toplevel.context_of;
|
file |
diff |
annotate
|
| Tue, 28 Nov 2006 00:35:21 +0100 |
wenzelm |
dest_term: strip_imp_concl;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 22:38:30 +0100 |
wenzelm |
prefer Proof.context over Context.generic;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:33 +0100 |
wenzelm |
moved theorem kinds from PureThy to Thm;
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 00:15:38 +0100 |
wenzelm |
incorporated IsarThy into IsarCmd;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2006 22:57:32 +0200 |
wenzelm |
renamed print_lthms to print_facts, do not insist on proof state;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 22:55:15 +0200 |
wenzelm |
removed 'undo_end', recovered 'cannot_undo';
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 00:27:30 +0200 |
wenzelm |
undo_end/kill: handle local theory;
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 19:37:06 +0200 |
wenzelm |
Secure.commit;
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 21:39:29 +0200 |
wenzelm |
added undo_end;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:26 +0200 |
wenzelm |
'print_theory': bang option for full verbosity;
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 19:12:46 +0200 |
wenzelm |
added class_deps;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:08 +0200 |
wenzelm |
ProofDisplay.print_theorems/theory;
|
file |
diff |
annotate
|
| Sun, 09 Apr 2006 18:51:20 +0200 |
wenzelm |
print_term etc.: actually observe print mode in final output;
|
file |
diff |
annotate
|
| Tue, 14 Mar 2006 22:06:37 +0100 |
wenzelm |
added print_stmts;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:07 +0100 |
wenzelm |
simplified presentation commands;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:09 +0100 |
wenzelm |
Locale.init;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:38 +0100 |
wenzelm |
print rules: generic context;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2006 22:29:59 +0100 |
wenzelm |
tuned print_theorems_theory;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 16:26:50 +0100 |
wenzelm |
Element.context;
|
file |
diff |
annotate
|
| Wed, 02 Nov 2005 14:47:00 +0100 |
wenzelm |
Isar.loop;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:32 +0200 |
wenzelm |
back: Toplevel.actual/skip_proof;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:36 +0200 |
wenzelm |
Proof.get_thmss;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 17:38:20 +0200 |
wenzelm |
add_chapter/section/subsection/subsubsection/text: optional locale specification;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 09:50:58 +0200 |
ballarin |
print_locale omits facts by default
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:45 +0200 |
wenzelm |
present_text: Toplevel.no_body_context prevents use of wrong context in interaction;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2005 12:07:00 +0200 |
ballarin |
Printing of interpretations: option to show witness theorems;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:37 +0200 |
wenzelm |
back: removed ill-defined '!' option;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:34 +0200 |
wenzelm |
Toplevel.actual_proof;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:14:13 +0200 |
wenzelm |
print_theorems: proper use of PureThy.print_theorems_diff;
|
file |
diff |
annotate
|
| Sun, 05 Jun 2005 11:31:21 +0200 |
wenzelm |
File.shell_path;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2005 18:29:53 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Mon, 23 May 2005 14:56:35 +0200 |
wenzelm |
use: not a theory command!
|
file |
diff |
annotate
|
| Sun, 22 May 2005 19:26:17 +0200 |
wenzelm |
string FindTheorems.criterion;
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:14 +0200 |
wenzelm |
added print_simpset;
|
file |
diff |
annotate
|
| Tue, 17 May 2005 18:10:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 16 May 2005 09:35:05 +0200 |
kleing |
searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 19:16:19 +0200 |
berghofe |
Adapted use command to new behaviour of Toplevel.node_trans
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:46:30 +0200 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|