Thu, 03 Jul 2008 11:16:05 +0200 |
haftmann |
adjusted rep_datatype
|
changeset |
files
|
Thu, 03 Jul 2008 00:58:30 +0200 |
berghofe |
Adapted to changes in perm_simp / swap_simps.
|
changeset |
files
|
Thu, 03 Jul 2008 00:56:45 +0200 |
berghofe |
Replaced all but one occurrence of perm_simp_tac by perm_simproc_app,
|
changeset |
files
|
Thu, 03 Jul 2008 00:54:45 +0200 |
berghofe |
Rewrote code to use swap_simps rather than calc_atm (which tends to
|
changeset |
files
|
Wed, 02 Jul 2008 21:43:57 +0200 |
wenzelm |
moved HOL-Plain up;
|
changeset |
files
|
Wed, 02 Jul 2008 20:31:06 +0200 |
wenzelm |
rename Doc doc-src;
|
changeset |
files
|
Wed, 02 Jul 2008 20:13:32 +0200 |
wenzelm |
renamed Contents to Dirs to avoid case-conflict with doc/Contents;
|
changeset |
files
|
Wed, 02 Jul 2008 19:52:57 +0200 |
huffman |
section -> subsection
|
changeset |
files
|
Wed, 02 Jul 2008 19:52:38 +0200 |
wenzelm |
convert Isabelle CVS to Mercurial;
|
changeset |
files
|
Wed, 02 Jul 2008 19:35:43 +0200 |
huffman |
use begin and end for proofs in locales
|
changeset |
files
|
Wed, 02 Jul 2008 18:13:10 +0200 |
wenzelm |
exclude Distribution/bin/Isabelle;
|
changeset |
files
|
Wed, 02 Jul 2008 16:40:20 +0200 |
wenzelm |
init_theory: pass name explicitly;
|
changeset |
files
|
Wed, 02 Jul 2008 16:40:18 +0200 |
wenzelm |
replaced datatype category constructivism by is_theory/is_proof;
|
changeset |
files
|
Wed, 02 Jul 2008 16:40:17 +0200 |
wenzelm |
Toplevel.init_theory: pass name explicitly;
|
changeset |
files
|
Wed, 02 Jul 2008 16:40:15 +0200 |
wenzelm |
command: always keep transition, not just as initial status;
|
changeset |
files
|
Wed, 02 Jul 2008 11:47:27 +0200 |
haftmann |
cached code for code antiquotation
|
changeset |
files
|
Wed, 02 Jul 2008 07:12:17 +0200 |
haftmann |
code antiquotation roaring ahead
|
changeset |
files
|
Wed, 02 Jul 2008 07:11:57 +0200 |
haftmann |
cleaned up some code generator configuration
|
changeset |
files
|
Tue, 01 Jul 2008 21:30:12 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
Tue, 01 Jul 2008 21:30:11 +0200 |
wenzelm |
added datatype category;
|
changeset |
files
|
Tue, 01 Jul 2008 21:30:08 +0200 |
wenzelm |
replaced datatype kind by OuterKeyword.category;
|
changeset |
files
|
Tue, 01 Jul 2008 21:20:18 +0200 |
wenzelm |
clean: HOL-Plain;
|
changeset |
files
|
Tue, 01 Jul 2008 20:26:48 +0200 |
huffman |
prove lemma finite in context of finite class
|
changeset |
files
|
Tue, 01 Jul 2008 20:10:59 +0200 |
wenzelm |
added HOL-Plain;
|
changeset |
files
|
Tue, 01 Jul 2008 18:38:44 +0200 |
wenzelm |
explicit identification of toplevel commands, with status etc.;
|
changeset |
files
|
Tue, 01 Jul 2008 18:38:43 +0200 |
wenzelm |
added name_of;
|
changeset |
files
|
Tue, 01 Jul 2008 18:38:41 +0200 |
wenzelm |
added get_id/put_id;
|
changeset |
files
|
Tue, 01 Jul 2008 09:58:32 +0200 |
haftmann |
(removed Complex/ROOT.ML)
|
changeset |
files
|
Tue, 01 Jul 2008 08:19:00 +0200 |
haftmann |
HOL += HOL-Complex
|
changeset |
files
|
Tue, 01 Jul 2008 08:05:08 +0200 |
haftmann |
HOL += HOL-Complex
|
changeset |
files
|