Thu, 07 Jul 2005 18:20:08 +0200 | huffman | use theorems ch2ch_cont, cont2contlubE | file | diff | annotate |
Fri, 01 Jul 2005 01:48:37 +0200 | huffman | cleaned up; added adm_less to adm_lemmas; added subsection headings | file | diff | annotate |
Sat, 25 Jun 2005 01:09:14 +0200 | huffman | cleaned up | file | diff | annotate |
Fri, 03 Jun 2005 23:15:16 +0200 | huffman | changed to work with new contlubE rule | file | diff | annotate |
Thu, 26 May 2005 00:30:24 +0200 | huffman | moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun | file | diff | annotate |
Wed, 25 May 2005 09:44:34 +0200 | wenzelm | removed LICENCE note -- everything is subject to Isabelle licence as | file | diff | annotate |
Tue, 24 May 2005 10:55:11 +0200 | paulson | cannot have files named adm.ML and Adm.ML on Macs, so deleted one and renamed the other | file | diff | annotate |
Tue, 24 May 2005 05:03:54 +0200 | huffman | Moved admissibility definitions and lemmas to a separate theory | file | diff | annotate |