| 2006-11-13 |
wenzelm |
recdef_tc(_i): local_theory interface via Specification.theorem_i;
|
changeset |
files
|
| 2006-11-13 |
wenzelm |
incorporated IsarThy into IsarCmd;
|
changeset |
files
|
| 2006-11-13 |
wenzelm |
removed theorem(_i);
|
changeset |
files
|
| 2006-11-13 |
haftmann |
upd
|
changeset |
files
|
| 2006-11-13 |
kleing |
atbroy51 broke down, switch to atbroy9
|
changeset |
files
|
| 2006-11-13 |
krauss |
updated
|
changeset |
files
|
| 2006-11-13 |
wenzelm |
antiquotation "theory": proper output, only check via ThyInfo.theory;
|
changeset |
files
|
| 2006-11-13 |
wenzelm |
tuned;
|
changeset |
files
|
| 2006-11-13 |
wenzelm |
added antiquotation @{theory name};
|
changeset |
files
|
| 2006-11-13 |
wenzelm |
fixed comment -- oops;
|
changeset |
files
|
| 2006-11-13 |
haftmann |
adjusted to new fun''
|
changeset |
files
|
| 2006-11-13 |
haftmann |
*** empty log message ***
|
changeset |
files
|
| 2006-11-13 |
haftmann |
added antiquotation theory
|
changeset |
files
|
| 2006-11-13 |
haftmann |
cleaned up
|
changeset |
files
|
| 2006-11-13 |
haftmann |
added theory antiquotation
|
changeset |
files
|
| 2006-11-13 |
haftmann |
combinator for overwriting changes with warning
|
changeset |
files
|
| 2006-11-13 |
haftmann |
added higher-order combinators for structured results
|
changeset |
files
|
| 2006-11-13 |
haftmann |
adjusted name in generated code
|
changeset |
files
|
| 2006-11-13 |
haftmann |
dropped LOrder dependency
|
changeset |
files
|
| 2006-11-13 |
haftmann |
moved upwars in HOL theory graph
|
changeset |
files
|
| 2006-11-13 |
haftmann |
added thy dependencies
|
changeset |
files
|
| 2006-11-13 |
haftmann |
PreList = Main - List
|
changeset |
files
|
| 2006-11-13 |
haftmann |
introduces preorders
|
changeset |
files
|
| 2006-11-13 |
haftmann |
dropped Inductive dependency
|
changeset |
files
|
| 2006-11-13 |
haftmann |
dropped Typedef dependency
|
changeset |
files
|
| 2006-11-13 |
haftmann |
added LOrder dependency
|
changeset |
files
|
| 2006-11-13 |
haftmann |
tuned ml antiquotations
|
changeset |
files
|
| 2006-11-13 |
haftmann |
adjusted
|
changeset |
files
|
| 2006-11-13 |
haftmann |
tuned
|
changeset |
files
|
| 2006-11-13 |
haftmann |
added tt tag
|
changeset |
files
|
| 2006-11-13 |
krauss |
auto_term => lexicographic_order
|
changeset |
files
|
| 2006-11-13 |
krauss |
updated
|
changeset |
files
|
| 2006-11-13 |
krauss |
replaced "auto_term" by the simpler method "relation", which does not try
|
changeset |
files
|
| 2006-11-13 |
wenzelm |
added fresh_prodD, which is included fresh_prodD into mksimps setup;
|
changeset |
files
|
| 2006-11-13 |
krauss |
added lexicographic_order.ML to makefile
|
changeset |
files
|
| 2006-11-12 |
nipkow |
image_constant_conv no longer [simp]
|
changeset |
files
|
| 2006-11-12 |
wenzelm |
instantiate: tuned indentity case;
|
changeset |
files
|
| 2006-11-12 |
wenzelm |
removed dead code;
|
changeset |
files
|
| 2006-11-12 |
wenzelm |
mk_atomize: careful matching against rules admits overloading;
|
changeset |
files
|
| 2006-11-12 |
nipkow |
started reorgnization of lattice theories
|
changeset |
files
|
| 2006-11-11 |
mengj |
Added in is_fol_thms.
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
level: do not account for local theory blocks (relevant for document preparation);
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
local 'end': no default tags;
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
* Local theory targets ``context/locale/class ... begin'' followed by ``end''.
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
removed obsolete context;
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
turned 'context' into plain thy_decl, discontinued thy_switch;
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
updated local theory targets;
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
updated local theory targets;
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
updated;
|
changeset |
files
|
| 2006-11-11 |
wenzelm |
Update standard keyword files.
|
changeset |
files
|
| 2006-11-10 |
wenzelm |
tuned comments;
|
changeset |
files
|
| 2006-11-10 |
wenzelm |
tuned comments;
|
changeset |
files
|
| 2006-11-10 |
wenzelm |
tuned names of start_timing,/end_timing/check_timer;
|
changeset |
files
|
| 2006-11-10 |
wenzelm |
removed obsolete ML compatibility fragments;
|
changeset |
files
|
| 2006-11-10 |
wenzelm |
avoid strange typing problem in MosML;
|
changeset |
files
|
| 2006-11-10 |
wenzelm |
tuned names of start_timing,/end_timing/check_timer;
|
changeset |
files
|
| 2006-11-10 |
wenzelm |
simplified local theory wrappers;
|
changeset |
files
|
| 2006-11-10 |
wenzelm |
removed mapping;
|
changeset |
files
|
| 2006-11-10 |
wenzelm |
simplified exit;
|
changeset |
files
|