equal
deleted
inserted
replaced
7 |
7 |
8 theory HOLCF |
8 theory HOLCF |
9 imports Sprod Ssum Up Lift Discrete One Tr Domain Main |
9 imports Sprod Ssum Up Lift Discrete One Tr Domain Main |
10 uses |
10 uses |
11 "holcf_logic.ML" |
11 "holcf_logic.ML" |
12 "cont_consts.ML" |
12 "Tools/cont_consts.ML" |
13 "domain/library.ML" |
13 "Tools/domain/domain_library.ML" |
14 "domain/syntax.ML" |
14 "Tools/domain/domain_syntax.ML" |
15 "domain/axioms.ML" |
15 "Tools/domain/domain_axioms.ML" |
16 "domain/theorems.ML" |
16 "Tools/domain/domain_theorems.ML" |
17 "domain/extender.ML" |
17 "Tools/domain/domain_extender.ML" |
18 "adm_tac.ML" |
18 "Tools/adm_tac.ML" |
19 |
19 |
20 begin |
20 begin |
21 |
21 |
22 ML_setup {* |
22 ML_setup {* |
23 change_simpset (fn simpset => simpset addSolver |
23 change_simpset (fn simpset => simpset addSolver |