| Sat, 02 Feb 2008 03:26:40 +0100 | huffman | cleaned up | changeset | files |
| Fri, 01 Feb 2008 18:01:06 +0100 | nipkow | modified MCollect syntax | changeset | files |
| Fri, 01 Feb 2008 08:35:58 +0100 | haftmann | <TERM> syntax | changeset | files |
| Fri, 01 Feb 2008 08:32:26 +0100 | haftmann | fixed term_of_sort | changeset | files |
| Fri, 01 Feb 2008 08:32:10 +0100 | haftmann | fixed record problem | changeset | files |
| Fri, 01 Feb 2008 02:38:41 +0100 | huffman | add lemmas prod_lessI and Pair_less_iff [simp] | changeset | files |
| Thu, 31 Jan 2008 22:00:31 +0100 | huffman | add lemma is_lub_lambda | changeset | files |
| Thu, 31 Jan 2008 21:48:14 +0100 | huffman | add lemma cpo_lubI | changeset | files |
| Thu, 31 Jan 2008 21:37:20 +0100 | huffman | add lemma cpo_lubI | changeset | files |
| Thu, 31 Jan 2008 21:23:14 +0100 | huffman | instances for class discrete_cpo | changeset | files |
| Thu, 31 Jan 2008 21:22:03 +0100 | huffman | new lemma cont_discrete_cpo | changeset | files |
| Thu, 31 Jan 2008 21:21:22 +0100 | huffman | new discrete_cpo axclass | changeset | files |
| Thu, 31 Jan 2008 11:47:12 +0100 | haftmann | temporary adjustions | changeset | files |
| Thu, 31 Jan 2008 11:44:46 +0100 | haftmann | explicit del_funcs | changeset | files |
| Thu, 31 Jan 2008 11:44:43 +0100 | haftmann | proper term_of functions | changeset | files |
| Thu, 31 Jan 2008 09:16:01 +0100 | haftmann | avoiding dynamic simpset lookup | changeset | files |
| Thu, 31 Jan 2008 01:31:19 +0100 | huffman | new lemma is_lub_Pair; cleaned up some proofs | changeset | files |
| Wed, 30 Jan 2008 17:36:03 +0100 | nipkow | commented stuff out | changeset | files |
| Wed, 30 Jan 2008 17:34:21 +0100 | nipkow | added multiset comprehension | changeset | files |
| Wed, 30 Jan 2008 10:57:47 +0100 | haftmann | idempotent semigroups | changeset | files |
| Wed, 30 Jan 2008 10:57:46 +0100 | haftmann | dual orders and dual lattices | changeset | files |
| Wed, 30 Jan 2008 10:57:44 +0100 | haftmann | Theorem Inductive.lfp_ordinal_induct generalized to complete lattices | changeset | files |
| Tue, 29 Jan 2008 18:00:12 +0100 | huffman | new term-building combinators | changeset | files |
| Tue, 29 Jan 2008 10:20:00 +0100 | haftmann | cleaned up evaluation interfaces | changeset | files |
| Tue, 29 Jan 2008 10:19:58 +0100 | haftmann | tuned names | changeset | files |
| Tue, 29 Jan 2008 10:19:56 +0100 | haftmann | treating division by zero properly | changeset | files |
| Mon, 28 Jan 2008 22:27:29 +0100 | wenzelm | eliminated escaped white space; | changeset | files |
| Mon, 28 Jan 2008 22:27:27 +0100 | wenzelm | basic scanners: produce symbol list instead of imploded string; | changeset | files |
| Mon, 28 Jan 2008 22:27:27 +0100 | wenzelm | * Outer syntax: string tokens no longer admit escaped white space; | changeset | files |
| Mon, 28 Jan 2008 22:27:26 +0100 | wenzelm | location_of_position: Position.column_of (which counts Isabelle symbols, not characters); | changeset | files |