| Sat, 17 Sep 2005 19:12:58 +0200 |
wenzelm |
manually generated from Isabelle/HOLCF/IOA/Complex/Import;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:25:11 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:24:57 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:30 +0200 |
wenzelm |
added with_charset: string -> ('a -> 'b) -> 'a -> 'b;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:29 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:28 +0200 |
wenzelm |
pretty_thm_aux: aconv hyps;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:27 +0200 |
wenzelm |
removed obsolete BasisLibrary;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:26 +0200 |
wenzelm |
Hebrew: HTML.with_charset;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:25 +0200 |
wenzelm |
removed obsolete BasisLibrary;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:24 +0200 |
wenzelm |
added quickcheck_params (from Main.thy);
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:23 +0200 |
wenzelm |
removed spurious PolyML.exception_trace;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:22 +0200 |
wenzelm |
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:21 +0200 |
wenzelm |
minor cleanup, moved stuff in its proper place;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:20 +0200 |
wenzelm |
generate: added HOL-Complex-Generate-HOLLight;
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:19 +0200 |
wenzelm |
added code generator setup (from Main.thy);
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:18 +0200 |
wenzelm |
lemmas [code] = imp_conv_disj (from Main.thy) -- Why does it need Datatype?
|
changeset |
files
|
| Sat, 17 Sep 2005 18:11:17 +0200 |
wenzelm |
HTML.with_charset;
|
changeset |
files
|
| Sat, 17 Sep 2005 17:35:26 +0200 |
wenzelm |
converted to Isar theory format;
|
changeset |
files
|
| Sat, 17 Sep 2005 14:02:31 +0200 |
wenzelm |
tuned document;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:51:03 +0200 |
wenzelm |
obsolete;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:50:57 +0200 |
wenzelm |
plain test session, includes example;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:08 +0200 |
wenzelm |
theory_to_proof: check theory of initial proof state, which must not be changed;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:07 +0200 |
wenzelm |
added auto_fix (from proof.ML);
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:06 +0200 |
wenzelm |
export put_facts;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:05 +0200 |
wenzelm |
interpretation: use goal commands without target -- no storing of results;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:04 +0200 |
wenzelm |
theorem(_i): empty target;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:03 +0200 |
wenzelm |
pretty_thm_aux: observe asms context;
|
changeset |
files
|
| Sat, 17 Sep 2005 12:18:02 +0200 |
wenzelm |
tuned;
|
changeset |
files
|