| Tue, 14 Nov 2006 00:15:38 +0100 | wenzelm | incorporated IsarThy into IsarCmd; | changeset | files |
| Tue, 14 Nov 2006 00:15:37 +0100 | wenzelm | removed theorem(_i); | changeset | files |
| Mon, 13 Nov 2006 22:31:23 +0100 | haftmann | upd | changeset | files |
| Mon, 13 Nov 2006 22:21:09 +0100 | kleing | atbroy51 broke down, switch to atbroy9 | changeset | files |
| Mon, 13 Nov 2006 21:52:14 +0100 | krauss | updated | changeset | files |
| Mon, 13 Nov 2006 20:10:02 +0100 | wenzelm | antiquotation "theory": proper output, only check via ThyInfo.theory; | changeset | files |
| Mon, 13 Nov 2006 20:08:52 +0100 | wenzelm | tuned; | changeset | files |
| Mon, 13 Nov 2006 20:08:20 +0100 | wenzelm | added antiquotation @{theory name}; | changeset | files |
| Mon, 13 Nov 2006 18:19:24 +0100 | wenzelm | fixed comment -- oops; | changeset | files |
| Mon, 13 Nov 2006 15:55:38 +0100 | haftmann | adjusted to new fun'' | changeset | files |
| Mon, 13 Nov 2006 15:45:34 +0100 | haftmann | *** empty log message *** | changeset | files |
| Mon, 13 Nov 2006 15:43:24 +0100 | haftmann | added antiquotation theory | changeset | files |
| Mon, 13 Nov 2006 15:43:16 +0100 | haftmann | cleaned up | changeset | files |
| Mon, 13 Nov 2006 15:43:15 +0100 | haftmann | added theory antiquotation | changeset | files |
| Mon, 13 Nov 2006 15:43:14 +0100 | haftmann | combinator for overwriting changes with warning | changeset | files |
| Mon, 13 Nov 2006 15:43:13 +0100 | haftmann | added higher-order combinators for structured results | changeset | files |
| Mon, 13 Nov 2006 15:43:12 +0100 | haftmann | adjusted name in generated code | changeset | files |
| Mon, 13 Nov 2006 15:43:11 +0100 | haftmann | dropped LOrder dependency | changeset | files |
| Mon, 13 Nov 2006 15:43:09 +0100 | haftmann | moved upwars in HOL theory graph | changeset | files |
| Mon, 13 Nov 2006 15:43:08 +0100 | haftmann | added thy dependencies | changeset | files |
| Mon, 13 Nov 2006 15:43:07 +0100 | haftmann | PreList = Main - List | changeset | files |
| Mon, 13 Nov 2006 15:43:06 +0100 | haftmann | introduces preorders | changeset | files |
| Mon, 13 Nov 2006 15:43:05 +0100 | haftmann | dropped Inductive dependency | changeset | files |
| Mon, 13 Nov 2006 15:43:04 +0100 | haftmann | dropped Typedef dependency | changeset | files |
| Mon, 13 Nov 2006 15:43:03 +0100 | haftmann | added LOrder dependency | changeset | files |
| Mon, 13 Nov 2006 15:43:00 +0100 | haftmann | tuned ml antiquotations | changeset | files |
| Mon, 13 Nov 2006 15:42:59 +0100 | haftmann | adjusted | changeset | files |
| Mon, 13 Nov 2006 15:42:58 +0100 | haftmann | tuned | changeset | files |
| Mon, 13 Nov 2006 15:42:57 +0100 | haftmann | added tt tag | changeset | files |
| Mon, 13 Nov 2006 15:01:59 +0100 | krauss | auto_term => lexicographic_order | changeset | files |
| Mon, 13 Nov 2006 13:53:48 +0100 | krauss | updated | changeset | files |
| Mon, 13 Nov 2006 13:51:22 +0100 | krauss | replaced "auto_term" by the simpler method "relation", which does not try | changeset | files |
| Mon, 13 Nov 2006 12:10:49 +0100 | wenzelm | added fresh_prodD, which is included fresh_prodD into mksimps setup; | changeset | files |
| Mon, 13 Nov 2006 11:41:40 +0100 | krauss | added lexicographic_order.ML to makefile | changeset | files |
| Sun, 12 Nov 2006 21:31:52 +0100 | nipkow | image_constant_conv no longer [simp] | changeset | files |
| Sun, 12 Nov 2006 21:14:52 +0100 | wenzelm | instantiate: tuned indentity case; | changeset | files |
| Sun, 12 Nov 2006 21:14:51 +0100 | wenzelm | removed dead code; | changeset | files |
| Sun, 12 Nov 2006 21:14:49 +0100 | wenzelm | mk_atomize: careful matching against rules admits overloading; | changeset | files |
| Sun, 12 Nov 2006 19:22:10 +0100 | nipkow | started reorgnization of lattice theories | changeset | files |
| Sat, 11 Nov 2006 23:58:46 +0100 | mengj | Added in is_fol_thms. | changeset | files |
| Sat, 11 Nov 2006 21:13:12 +0100 | wenzelm | level: do not account for local theory blocks (relevant for document preparation); | changeset | files |
| Sat, 11 Nov 2006 21:13:11 +0100 | wenzelm | local 'end': no default tags; | changeset | files |
| Sat, 11 Nov 2006 16:12:23 +0100 | wenzelm | * Local theory targets ``context/locale/class ... begin'' followed by ``end''. | changeset | files |
| Sat, 11 Nov 2006 16:11:44 +0100 | wenzelm | removed obsolete context; | changeset | files |
| Sat, 11 Nov 2006 16:11:43 +0100 | wenzelm | turned 'context' into plain thy_decl, discontinued thy_switch; | changeset | files |
| Sat, 11 Nov 2006 16:11:42 +0100 | wenzelm | tuned proofs; | changeset | files |
| Sat, 11 Nov 2006 16:11:41 +0100 | wenzelm | updated local theory targets; | changeset | files |
| Sat, 11 Nov 2006 16:11:40 +0100 | wenzelm | updated local theory targets; | changeset | files |
| Sat, 11 Nov 2006 16:11:39 +0100 | wenzelm | updated; | changeset | files |
| Sat, 11 Nov 2006 14:52:25 +0100 | wenzelm | Update standard keyword files. | changeset | files |
| Fri, 10 Nov 2006 23:22:12 +0100 | wenzelm | tuned comments; | changeset | files |
| Fri, 10 Nov 2006 23:22:11 +0100 | wenzelm | tuned comments; | changeset | files |
| Fri, 10 Nov 2006 23:22:10 +0100 | wenzelm | tuned names of start_timing,/end_timing/check_timer; | changeset | files |
| Fri, 10 Nov 2006 23:22:04 +0100 | wenzelm | removed obsolete ML compatibility fragments; | changeset | files |
| Fri, 10 Nov 2006 23:22:03 +0100 | wenzelm | avoid strange typing problem in MosML; | changeset | files |
| Fri, 10 Nov 2006 23:22:01 +0100 | wenzelm | tuned names of start_timing,/end_timing/check_timer; | changeset | files |
| Fri, 10 Nov 2006 22:18:54 +0100 | wenzelm | simplified local theory wrappers; | changeset | files |
| Fri, 10 Nov 2006 22:18:53 +0100 | wenzelm | removed mapping; | changeset | files |
| Fri, 10 Nov 2006 22:18:52 +0100 | wenzelm | simplified exit; | changeset | files |
| Fri, 10 Nov 2006 22:18:51 +0100 | wenzelm | simplified LocalTheory.exit; | changeset | files |