| Fri, 12 Oct 2007 14:42:30 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 12 Oct 2007 14:42:29 +0200 |
haftmann |
(intermediate quickfix)
|
changeset |
files
|
| Fri, 12 Oct 2007 10:29:02 +0200 |
haftmann |
removed
|
changeset |
files
|
| Fri, 12 Oct 2007 10:26:18 +0200 |
haftmann |
added
|
changeset |
files
|
| Fri, 12 Oct 2007 10:24:49 +0200 |
paulson |
metis calls
|
changeset |
files
|
| Fri, 12 Oct 2007 08:31:57 +0200 |
haftmann |
updated
|
changeset |
files
|
| Fri, 12 Oct 2007 08:25:48 +0200 |
haftmann |
moved class power to theory Power
|
changeset |
files
|
| Fri, 12 Oct 2007 08:25:47 +0200 |
haftmann |
refined; moved class power to theory Power
|
changeset |
files
|
| Fri, 12 Oct 2007 08:21:09 +0200 |
haftmann |
consolidated naming conventions for code generator theories
|
changeset |
files
|
| Fri, 12 Oct 2007 08:20:46 +0200 |
haftmann |
class div inherits from class times
|
changeset |
files
|
| Fri, 12 Oct 2007 08:20:45 +0200 |
haftmann |
code_include replaces code_moduleprolog
|
changeset |
files
|
| Fri, 12 Oct 2007 08:20:43 +0200 |
haftmann |
added subclass command
|
changeset |
files
|
| Thu, 11 Oct 2007 23:03:51 +0200 |
wenzelm |
enabled Refute_Examples again;
|
changeset |
files
|
| Thu, 11 Oct 2007 23:03:11 +0200 |
wenzelm |
local_axioms: impose hyps stemming from local consts as well
|
changeset |
files
|
| Thu, 11 Oct 2007 21:44:28 +0200 |
wenzelm |
disabled Refute_Examples temporarily;
|
changeset |
files
|
| Thu, 11 Oct 2007 21:10:43 +0200 |
wenzelm |
local_theory: incorporated consts into axioms;
|
changeset |
files
|
| Thu, 11 Oct 2007 21:10:42 +0200 |
wenzelm |
removed unused/impure quiet_mode;
|
changeset |
files
|
| Thu, 11 Oct 2007 21:10:41 +0200 |
wenzelm |
added export_cterm;
|
changeset |
files
|
| Thu, 11 Oct 2007 21:10:40 +0200 |
wenzelm |
local_theory: incorporated consts into axioms;
|
changeset |
files
|
| 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
|