| Sat, 15 Nov 2008 21:31:21 +0100 |
wenzelm |
pretty_thm: oracle flag is always false for now (would require detailed check wrt. promises);
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:20 +0100 |
wenzelm |
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:19 +0100 |
wenzelm |
name_of_thm: Proofterm.fold_proof_atoms;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:17 +0100 |
wenzelm |
Thm.proof_of returns proof_body;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:15 +0100 |
wenzelm |
clean: added HOL-Main;
|
changeset |
files
|
| Sat, 15 Nov 2008 21:31:13 +0100 |
wenzelm |
rewrite_proof: simplified simprocs (no name required);
|
changeset |
files
|
| Sat, 15 Nov 2008 11:25:17 +0100 |
wenzelm |
multithreading support for polyml-5.2 actually disabled -- as advertized;
|
changeset |
files
|
| Fri, 14 Nov 2008 16:49:52 +0100 |
ballarin |
Initial part of locale reimplementation.
|
changeset |
files
|
| Fri, 14 Nov 2008 14:00:52 +0100 |
ballarin |
Made local_note_prefix public.
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:11 +0100 |
haftmann |
re-educated guess
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:10 +0100 |
haftmann |
namify and name_decl combinators
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:09 +0100 |
haftmann |
Name.is_nothing
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:08 +0100 |
haftmann |
lemmas about dom and minus / insert
|
changeset |
files
|
| Fri, 14 Nov 2008 08:50:07 +0100 |
haftmann |
added length_unique operation for code generation
|
changeset |
files
|
| Thu, 13 Nov 2008 22:45:12 +0100 |
wenzelm |
updated generated files;
|
changeset |
files
|