| Thu, 11 Oct 2007 19:10:25 +0200 |
wenzelm |
replaced Term.equiv_types by Type.similar_types;
|
changeset |
files
|
| Thu, 11 Oct 2007 19:10:24 +0200 |
wenzelm |
replaced Term.equiv_types by Type.similar_types;
|
changeset |
files
|
| Thu, 11 Oct 2007 19:10:23 +0200 |
wenzelm |
dest/cert_def: replaced Pretty.pp by explicit Proof.context;
|
changeset |
files
|
| Thu, 11 Oct 2007 19:10:22 +0200 |
wenzelm |
added elim_implies (more convenient argument order);
|
changeset |
files
|
| Thu, 11 Oct 2007 19:10:21 +0200 |
wenzelm |
removed obsolete flip;
|
changeset |
files
|
| Thu, 11 Oct 2007 19:10:20 +0200 |
wenzelm |
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
|
changeset |
files
|
| Thu, 11 Oct 2007 19:10:19 +0200 |
wenzelm |
replaced (flip Thm.implies_elim) by Thm.elim_implies;
|
changeset |
files
|
| Thu, 11 Oct 2007 19:10:17 +0200 |
wenzelm |
moved Drule.unvarify to Thm.unvarify (cf. more_thm.ML);
|
changeset |
files
|
| Thu, 11 Oct 2007 18:58:34 +0200 |
wenzelm |
usedir: added HOL_USEDIR_OPTIONS;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:51:39 +0200 |
paulson |
reconstruction bug fix
|
changeset |
files
|
| Thu, 11 Oct 2007 16:38:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:38:42 +0200 |
wenzelm |
replaced Sign.add_consts_i by Sign.declare_const;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:56 +0200 |
wenzelm |
replaced Sign.add_consts_authentic by Sign.declare_const;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:53 +0200 |
wenzelm |
renamed Syntax.XXX_mode to Syntax.mode_XXX;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:47 +0200 |
wenzelm |
removed obsolete AxClass.params_of_class;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:44 +0200 |
wenzelm |
replaced Sign.add_consts_authentic by Sign.declare_const;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:41 +0200 |
wenzelm |
load axclass.ML before Isar;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:39 +0200 |
wenzelm |
added specify_const;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:37 +0200 |
wenzelm |
removed obsolete simple_def;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:35 +0200 |
wenzelm |
moved define_class_params to Isar/class.ML;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:33 +0200 |
wenzelm |
load axclass.ML before Isar;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:32 +0200 |
wenzelm |
Theory.specify_const;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:30 +0200 |
wenzelm |
moved ProofContext.pp to Syntax.pp;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:26 +0200 |
wenzelm |
renamed Syntax.XXX_mode to Syntax.mode_XXX;
|
changeset |
files
|
| Thu, 11 Oct 2007 16:05:23 +0200 |
wenzelm |
replaced Sign.add_consts_authentic by Sign.declare_const;
|
changeset |
files
|
| Thu, 11 Oct 2007 15:59:31 +0200 |
paulson |
rationalized redundant code
|
changeset |
files
|
| Thu, 11 Oct 2007 15:57:29 +0200 |
wenzelm |
usage: HOL_USEDIR_OPTIONS;
|
changeset |
files
|
| Thu, 11 Oct 2007 10:23:09 +0200 |
paulson |
failure messages
|
changeset |
files
|
| Thu, 11 Oct 2007 00:33:43 +0200 |
wenzelm |
'notation': allow structmixfix;
|
changeset |
files
|
| Thu, 11 Oct 2007 00:28:32 +0200 |
wenzelm |
update_modesyntax: may delete 'structure' notation as well;
|
changeset |
files
|