equal
deleted
inserted
replaced
10 Domain |
10 Domain |
11 Powerdomains |
11 Powerdomains |
12 begin |
12 begin |
13 |
13 |
14 default_sort "domain" |
14 default_sort "domain" |
15 |
|
16 ML {* Thy_Load.legacy_path_add "~~/src/HOL/HOLCF/Library" *} |
|
17 |
15 |
18 text {* Legacy theorem names deprecated after Isabelle2009-2: *} |
16 text {* Legacy theorem names deprecated after Isabelle2009-2: *} |
19 |
17 |
20 lemmas expand_fun_below = fun_below_iff |
18 lemmas expand_fun_below = fun_below_iff |
21 lemmas below_fun_ext = fun_belowI |
19 lemmas below_fun_ext = fun_belowI |