Mercurial
Mercurial
>
repos
>
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
src/HOLCF/Pcpo.ML
2005-07-26
huffman
brought ML files up to date with new lemmas
file
|
diff
|
annotate
2005-03-02
huffman
converted to new-style theory
file
|
diff
|
annotate
2004-06-21
kleing
Merged in license change from Isabelle2004
file
|
diff
|
annotate
2001-12-12
wenzelm
isatool expandshort;
file
|
diff
|
annotate
2001-11-03
wenzelm
GPLed;
file
|
diff
|
annotate
2001-05-31
oheimb
added lub_range_mono and lub_range_shift
file
|
diff
|
annotate
2000-09-15
paulson
renamed (most of...) the select rules
file
|
diff
|
annotate
2000-07-05
paulson
massive tidy-up: goal -> Goal, remove use of prems, etc.
file
|
diff
|
annotate
2000-06-28
paulson
tidying and unbatchifying
file
|
diff
|
annotate
1998-03-10
oheimb
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
file
|
diff
|
annotate
1997-11-03
wenzelm
isatool fixclasimp;
file
|
diff
|
annotate
1997-10-10
wenzelm
fixed dots;
file
|
diff
|
annotate
1997-09-29
paulson
fast_tac HOL_cs -> Fast_tac, etc.
file
|
diff
|
annotate
1997-05-25
slotosch
Moved the classes flat chfin from Fix to Pcpo.
file
|
diff
|
annotate
1997-05-25
slotosch
eliminated the constant less by the introduction of the axclass sq_ord
file
|
diff
|
annotate
1997-03-25
slotosch
changed some theorems from pcpo to cpo
file
|
diff
|
annotate
1997-02-17
slotosch
Changes of HOLCF from Oscar Slotosch:
file
|
diff
|
annotate
1996-12-18
oheimb
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
file
|
diff
|
annotate
1996-12-16
paulson
Removed a rogue TAB
file
|
diff
|
annotate
1996-12-13
oheimb
adaptions for symbol font
file
|
diff
|
annotate
1996-12-09
sandnerr
added theorems
file
|
diff
|
annotate
1996-11-29
oheimb
renamed is_flat to flat,
file
|
diff
|
annotate
1996-09-26
paulson
Ran expandshort; used stac instead of ssubst
file
|
diff
|
annotate
1996-05-31
oheimb
introduced forgotten bind_thm calls
file
|
diff
|
annotate
1996-04-23
oheimb
adapted several proofs
file
|
diff
|
annotate
1996-01-30
clasohm
expanded tabs
file
|
diff
|
annotate
1995-10-04
clasohm
added local simpsets
file
|
diff
|
annotate
1995-04-13
regensbu
adjusted HOLCF for new hyp_subst_tac
file
|
diff
|
annotate
1995-02-07
clasohm
added qed, qed_goal[w]
file
|
diff
|
annotate
1994-06-29
clasohm
added parentheses made necessary by change of constrain's precedence
file
|
diff
|
annotate
1994-01-19
nipkow
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
file
|
diff
|
annotate
less
more
(0)
tip