Mon, 05 Jan 2004 00:46:06 +0100 | nipkow | undid split_comp_eq[simp] because it leads to nontermination together with split_def! | changeset | files |
Sat, 03 Jan 2004 16:09:39 +0100 | paulson | Deleting more redundant theorems | changeset | files |
Thu, 01 Jan 2004 21:47:07 +0100 | paulson | conversion of Real/PReal to Isar script; | changeset | files |
Thu, 01 Jan 2004 10:06:32 +0100 | paulson | tweaking of lemmas in RealDef, RealOrd | changeset | files |
Mon, 29 Dec 2003 06:49:26 +0100 | kleing | \<^bsub> .. \<^esub> | changeset | files |
Mon, 29 Dec 2003 06:07:44 +0100 | kleing | spanning super and sub scripts \<^bsub> .. \<^esub> and \<^bsup> .. \<^esup> | changeset | files |