| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
| #
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def';
tuned comments;
|
| #
e64e636d |
|
13-Jan-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
e5735396 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
| #
6f4dc4fe |
|
07-Sep-2011 |
wenzelm <none@none> |
clarified import;
|
| #
91214357 |
|
29-Mar-2011 |
wenzelm <none@none> |
tuned headers;
|
| #
9d7c4f76 |
|
06-Jan-2011 |
huffman <none@none> |
rename constant u_defl to u_liftdefl;
add new constant u_defl :: udom defl -> udom defl
|
| #
94cce012 |
|
06-Jan-2011 |
huffman <none@none> |
rename constant pdefl to liftdefl_of
|
| #
0d03e994 |
|
19-Dec-2010 |
huffman <none@none> |
rename function cprod_map to prod_map
|
| #
d23730c2 |
|
19-Dec-2010 |
huffman <none@none> |
use deflations over type 'udom u' to represent predomains;
removed now-unnecessary class liftdomain;
|
| #
1f632c05 |
|
19-Dec-2010 |
huffman <none@none> |
replace foo_approx functions with foo_emb, foo_prj functions for universal domain embeddings
|
| #
7c56eb3d |
|
19-Dec-2010 |
huffman <none@none> |
type 'defl' takes a type parameter again (cf. b525988432e9)
|
| #
0e0045ed |
|
19-Dec-2010 |
huffman <none@none> |
reintroduce 'bifinite' class, now with existentially-quantified approx function (cf. b525988432e9)
|
| #
f4f6e1bf |
|
19-Dec-2010 |
huffman <none@none> |
renamed Bifinite.thy to Representable.thy
--HG--
rename : src/HOL/HOLCF/Bifinite.thy => src/HOL/HOLCF/Representable.thy
|