| 2010-11-10 |
huffman |
2010-11-10 |
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
|
file | diff | annotate |
| 2010-10-29 |
huffman |
2010-10-29 |
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
|
file | diff | annotate |
| 2010-10-22 |
huffman |
2010-10-22 |
remove finite_po class
|
file | diff | annotate |
| 2010-10-21 |
huffman |
2010-10-21 |
add type annotation to avoid warning
|
file | diff | annotate |
| 2010-10-21 |
huffman |
2010-10-21 |
simplify some proofs, convert to Isar style
|
file | diff | annotate |
| 2010-10-11 |
huffman |
2010-10-11 |
new theorem names: fun_below_iff, fun_belowI, cfun_eq_iff, cfun_eqI, cfun_below_iff, cfun_belowI
|
file | diff | annotate |
| 2010-10-09 |
huffman |
2010-10-09 |
move all bifinite class instances to Bifinite.thy
|
file | diff | annotate |
| 2010-10-08 |
huffman |
2010-10-08 |
rename class 'sfp' to 'bifinite'
|
file | diff | annotate |
| 2010-10-07 |
huffman |
2010-10-07 |
move stuff from Algebraic.thy to Bifinite.thy and elsewhere
|
file | diff | annotate |
| 2010-10-06 |
huffman |
2010-10-06 |
major reorganization/simplification of HOLCF type classes:
removed profinite/bifinite classes and approx function;
universal domain uses approx_chain locale instead of bifinite class;
ideal_completion locale does not use 'take' functions, requires countable basis instead;
replaced type 'udom alg_defl' with type 'sfp';
replaced class 'rep' with class 'sfp';
renamed REP('a) to SFP('a);
|
file | diff | annotate |
| 2010-10-05 |
Brian Huffman |
2010-10-05 |
add lemma finite_deflation_intro
|
file | diff | annotate |
| 2010-09-13 |
nipkow |
2010-09-13 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| 2010-09-07 |
nipkow |
2010-09-07 |
renamed expand_*_eq in HOLCF as well
|
file | diff | annotate |
| 2010-04-28 |
wenzelm |
2010-04-28 |
renamed command 'defaultsort' to 'default_sort';
|
file | diff | annotate |
| 2010-03-22 |
huffman |
2010-03-22 |
remove LaTeX hyperref warnings by avoiding antiquotations within section headings
|
file | diff | annotate |
| 2010-03-13 |
huffman |
2010-03-13 |
declare case_names for various induction rules
|
file | diff | annotate |
| 2010-03-02 |
wenzelm |
2010-03-02 |
proper (type_)notation;
|
file | diff | annotate |
| 2010-01-16 |
haftmann |
2010-01-16 |
dropped some old primrecs and some constdefs
|
file | diff | annotate |
| 2009-11-19 |
huffman |
2009-11-19 |
add map_ID lemmas
|
file | diff | annotate |
| 2009-11-09 |
huffman |
2009-11-09 |
add map_map lemmas
|
file | diff | annotate |
| 2009-11-05 |
huffman |
2009-11-05 |
map functions for various types, with ep_pair/deflation/finite_deflation lemmas
|
file | diff | annotate |
| 2009-05-08 |
huffman |
2009-05-08 |
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
|
file | diff | annotate |
| 2009-01-14 |
huffman |
2009-01-14 |
change to simpler, more extensible continuity simproc
define attribute [cont2cont] for continuity rules;
new continuity simproc just applies cont2cont rules repeatedly;
split theory Product_Cpo from Cprod, so Cfun can import Product_Cpo;
add lemma cont2cont_LAM', which is suitable as a cont2cont rule.
|
file | diff | annotate |
| 2008-12-16 |
huffman |
2008-12-16 |
remove cvs Id tags
|
file | diff | annotate |
| 2008-07-01 |
huffman |
2008-07-01 |
remove unused lemma is_lub_Iup'
|
file | diff | annotate |
| 2008-07-01 |
huffman |
2008-07-01 |
replace lub (range Y) with (LUB i. Y i)
|
file | diff | annotate |
| 2008-06-20 |
huffman |
2008-06-20 |
simplify profinite class axioms
|
file | diff | annotate |
| 2008-05-19 |
huffman |
2008-05-19 |
use new class package for classes profinite, bifinite; remove approx class
|
file | diff | annotate |
| 2008-03-26 |
huffman |
2008-03-26 |
rename class bifinite_cpo to profinite; generalize powerdomains from bifinite to profinite
|
file | diff | annotate |
| 2008-02-07 |
huffman |
2008-02-07 |
fix broken syntax translations
|
file | diff | annotate |
| 2008-01-31 |
huffman |
2008-01-31 |
add lemma cpo_lubI
|
file | diff | annotate |
| 2008-01-17 |
huffman |
2008-01-17 |
rename lemma chain_mono3 -> chain_mono, chain_mono -> chain_mono_less
|
file | diff | annotate |
| 2008-01-17 |
huffman |
2008-01-17 |
change class axiom chfin to rule_format
|
file | diff | annotate |
| 2008-01-14 |
huffman |
2008-01-14 |
added bifinite class instance
|
file | diff | annotate |
| 2008-01-14 |
huffman |
2008-01-14 |
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff
|
file | diff | annotate |
| 2008-01-14 |
huffman |
2008-01-14 |
compact_chfin is now declared simp
|
file | diff | annotate |
| 2008-01-10 |
huffman |
2008-01-10 |
new compactness lemmas
|
file | diff | annotate |
| 2008-01-04 |
huffman |
2008-01-04 |
new instance proofs for classes finite_po, chfin, flat
|
file | diff | annotate |
| 2008-01-02 |
huffman |
2008-01-02 |
add dcpo instance proof
|
file | diff | annotate |
| 2008-01-02 |
huffman |
2008-01-02 |
declare upE as cases rule; add new rule up_induct
|
file | diff | annotate |
| 2008-01-02 |
huffman |
2008-01-02 |
update sq_ord/po instance proofs
|
file | diff | annotate |
| 2008-01-02 |
huffman |
2008-01-02 |
remove not_up_less_UU [simp]
|
file | diff | annotate |
| 2007-10-21 |
wenzelm |
2007-10-21 |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file | diff | annotate |
| 2006-02-19 |
huffman |
2006-02-19 |
use minimal imports
|
file | diff | annotate |
| 2005-11-30 |
huffman |
2005-11-30 |
add xsymbol syntax for u type constructor
|
file | diff | annotate |
| 2005-11-03 |
huffman |
2005-11-03 |
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
|
file | diff | annotate |
| 2005-10-12 |
huffman |
2005-10-12 |
added compactness theorems
|
file | diff | annotate |
| 2005-09-22 |
huffman |
2005-09-22 |
cleaned up
|
file | diff | annotate |
| 2005-07-28 |
wenzelm |
2005-07-28 |
fixed var index in tactic;
|
file | diff | annotate |
| 2005-07-08 |
huffman |
2005-07-08 |
define 'a u with datatype package;
removed obsolete lemmas;
renamed upE1 to upE and Exh_Up1 to Exh_Up;
cleaned up
|
file | diff | annotate |
| 2005-06-23 |
huffman |
2005-06-23 |
add csplit3, ssplit3, fup3 as simp rules
|
file | diff | annotate |
| 2005-06-08 |
huffman |
2005-06-08 |
make up_eq and up_less into simp rules
|
file | diff | annotate |
| 2005-06-08 |
huffman |
2005-06-08 |
major cleanup: rewrote cpo proofs, removed obsolete lemmas, renamed some lemmas
|
file | diff | annotate |
| 2005-06-03 |
huffman |
2005-06-03 |
changed to use new contlubI, etc.
|
file | diff | annotate |
| 2005-05-25 |
wenzelm |
2005-05-25 |
removed LICENCE note -- everything is subject to Isabelle licence as
stated in COPYRIGHT file;
|
file | diff | annotate |
| 2005-03-10 |
huffman |
2005-03-10 |
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
|
file | diff | annotate |
| 2005-03-08 |
huffman |
2005-03-08 |
reordered and arranged for document generation, cleaned up some proofs
|
file | diff | annotate |
| 2005-03-04 |
huffman |
2005-03-04 |
fix headers
|
file | diff | annotate |
| 2005-03-04 |
huffman |
2005-03-04 |
converted to new-style theories, and combined numbered files
|
file | diff | annotate |