| Mon, 23 Jun 2008 23:45:45 +0200 |
wenzelm |
Logic.is_all;
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:55:04 +0200 |
wenzelm |
added emulations for simple_read_term/read_term/read_prop (formerly in sign.ML);
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 22:13:49 +0200 |
wenzelm |
removed obsolete no_qed, quick_and_dirty_prove_goalw_cterm;
|
file |
diff |
annotate
|
| Mon, 16 Jun 2008 17:54:47 +0200 |
wenzelm |
removed obsolete inst;
|
file |
diff |
annotate
|
| Wed, 11 Jun 2008 18:03:38 +0200 |
wenzelm |
qualified inst;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 18:49:19 +0200 |
wenzelm |
Theory.eq_thy;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2008 16:12:05 +0200 |
wenzelm |
Thm.forall_elim_var(s);
|
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, 27 Mar 2008 14:41:17 +0100 |
wenzelm |
moved old the_context here;
|
file |
diff |
annotate
|
| Wed, 26 Mar 2008 22:40:05 +0100 |
wenzelm |
moved bind_thm(s) to ML/ml_context.ML;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2008 22:07:32 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 23:26:27 +0100 |
wenzelm |
cond_timeit: added message argument;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 18:39:15 +0200 |
wenzelm |
removed obsolete disable_pr/enable_pr;
|
file |
diff |
annotate
|
| Mon, 04 Jun 2007 21:04:20 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 30 Apr 2007 13:32:58 +0200 |
wenzelm |
explicit treatment of legacy_features;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:35:52 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 23:18:24 +0100 |
wenzelm |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:18 +0100 |
wenzelm |
moved inst from drule.ML to old_goals.ML;
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:30:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 15:03:09 +0200 |
wenzelm |
removed OldGoals.legacy flag (always warn);
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:07 +0200 |
wenzelm |
Assumption.assume;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:04 +0100 |
wenzelm |
chop is no longer pervasive;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 10:43:11 +0100 |
wenzelm |
renamed goals.ML to old_goals.ML;
|
file |
diff |
annotate
|