| Wed, 27 Oct 2010 14:31:39 -0700 |
huffman |
add 'LAM (Def x). t' as alternative syntax for 'FLIFT x. t'
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 13:54:18 -0700 |
huffman |
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 06:58:45 -0700 |
huffman |
remove finite_po class
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 06:08:51 -0700 |
huffman |
simplify proofs about flift; remove unneeded lemmas
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 15:21:39 -0700 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Thu, 21 Oct 2010 06:03:18 -0700 |
huffman |
pcpodef (open) 'a lift
|
file |
diff |
annotate
|
| Tue, 12 Oct 2010 09:32:21 -0700 |
huffman |
remove unneeded lemmas Lift_exhaust, Lift_cases
|
file |
diff |
annotate
|
| Tue, 12 Oct 2010 09:08:27 -0700 |
huffman |
move lemmas from Lift.thy to Cfun.thy
|
file |
diff |
annotate
|
| Tue, 12 Oct 2010 06:20:05 -0700 |
huffman |
remove unneeded lemmas from Fun_Cpo.thy
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 21:35:31 -0700 |
huffman |
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
|
file |
diff |
annotate
|
| Sat, 09 Oct 2010 07:24:49 -0700 |
huffman |
move all bifinite class instances to Bifinite.thy
|
file |
diff |
annotate
|
| Fri, 08 Oct 2010 07:39:50 -0700 |
huffman |
rename class 'sfp' to 'bifinite'
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 10:49:27 -0700 |
huffman |
major reorganization/simplification of HOLCF type classes:
|
file |
diff |
annotate
|
| Sun, 23 May 2010 19:30:14 -0700 |
huffman |
declare a few more cont2cont rules
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:07:52 +0200 |
wenzelm |
renamed command 'defaultsort' to 'default_sort';
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 07:50:21 -0700 |
huffman |
remove ancient continuity tactic
|
file |
diff |
annotate
|
| Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
| Fri, 08 May 2009 16:19:51 -0700 |
huffman |
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
|
file |
diff |
annotate
|
| Fri, 20 Mar 2009 15:24:18 +0100 |
wenzelm |
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:31:55 -0800 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| Thu, 11 Dec 2008 16:50:18 +0100 |
wenzelm |
pcpodef package: state two goals, instead of encoded conjunction;
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 23:37:24 +0200 |
huffman |
remove unused constant liftpair
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 23:01:09 +0200 |
huffman |
simplify profinite class axioms
|
file |
diff |
annotate
|
| Fri, 20 Jun 2008 17:58:16 +0200 |
huffman |
tuned
|
file |
diff |
annotate
|
| Tue, 10 Jun 2008 15:30:33 +0200 |
haftmann |
rep_datatype command now takes list of constructors as input arguments
|
file |
diff |
annotate
|
| Mon, 19 May 2008 23:50:06 +0200 |
huffman |
instantiation lift :: (countable) bifinite
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 19:49:24 +0100 |
huffman |
declare cont_lemmas_ext as simp rules individually
|
file |
diff |
annotate
|
| Wed, 16 Jan 2008 22:41:49 +0100 |
huffman |
change class axiom ax_flat to rule_format
|
file |
diff |
annotate
|
| Fri, 04 Jan 2008 00:01:02 +0100 |
huffman |
new instance proofs for classes finite_po, chfin, flat
|
file |
diff |
annotate
|
| Thu, 20 Dec 2007 03:06:20 +0100 |
huffman |
move bottom-related stuff back into Pcpo.thy
|
file |
diff |
annotate
|
| Tue, 18 Dec 2007 22:18:31 +0100 |
huffman |
add class ppo of pointed partial orders;
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 14:21:48 +0200 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
| Fri, 02 Jun 2006 20:12:59 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Mon, 01 May 2006 01:22:31 +0200 |
huffman |
add theorem flift2_defined_iff
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 23:15:44 +0200 |
huffman |
add lemma less_UU_iff as default simp rule
|
file |
diff |
annotate
|
| Sat, 05 Nov 2005 21:50:37 +0100 |
huffman |
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:21:52 +0200 |
wenzelm |
adm_tac/cont_tacRs: proper simpset;
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 03:09:32 +0200 |
huffman |
replaced old continuity rules with new lemma cont2cont_lift_case
|
file |
diff |
annotate
|
| Fri, 08 Jul 2005 02:42:04 +0200 |
huffman |
renamed upE1 to upE; added simp rule cont2cont_flift1
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 21:41:08 +0200 |
huffman |
removed obsolete continuity theorems
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 21:22:15 +0200 |
huffman |
define lift type using pcpodef; cleaned up
|
file |
diff |
annotate
|
| Tue, 05 Jul 2005 23:14:48 +0200 |
huffman |
simplified definitions of flift1, flift2, liftpair;
|
file |
diff |
annotate
|
| Fri, 01 Jul 2005 04:09:27 +0200 |
huffman |
added theorem lift_definedE; moved cont_if to Cont.thy
|
file |
diff |
annotate
|
| Thu, 23 Jun 2005 22:10:29 +0200 |
huffman |
add binder syntax for flift1
|
file |
diff |
annotate
|
| Tue, 14 Jun 2005 04:05:15 +0200 |
huffman |
renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
|
file |
diff |
annotate
|
| Fri, 03 Jun 2005 23:35:18 +0200 |
huffman |
renamed variable in cont2cont_app
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 25 May 2005 02:49:46 +0200 |
huffman |
shorted proof that lift is chfin
|
file |
diff |
annotate
|
| Mon, 23 May 2005 23:24:38 +0200 |
huffman |
moved continuity simproc to Cont.thy
|
file |
diff |
annotate
|
| Fri, 06 May 2005 03:47:44 +0200 |
huffman |
Replaced all unnecessary uses of SOME with THE or LEAST
|
file |
diff |
annotate
|
| Sat, 02 Apr 2005 00:33:51 +0200 |
huffman |
Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 23:23:47 +0100 |
huffman |
fix headers
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 23:12:36 +0100 |
huffman |
converted to new-style theories, and combined numbered files
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Fri, 11 Jul 2003 13:54:26 +0200 |
oheimb |
corrected markup text
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:38:11 +0100 |
wenzelm |
rep_datatype lift;
|
file |
diff |
annotate
|
| Mon, 17 Feb 1997 10:57:11 +0100 |
slotosch |
Changes of HOLCF from Oscar Slotosch:
|
file |
diff |
annotate
|