equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 This is just an ad-hoc hack which will rarely give you what you want. |
13 This is just an ad-hoc hack which will rarely give you what you want. |
14 For the moment, whenever you need executable sets, consider using |
14 For the moment, whenever you need executable sets, consider using |
15 type @{text fset} from theory @{text Fset}. |
15 type @{text fset} from theory @{text Cset}. |
16 *} |
16 *} |
17 |
17 |
18 declare mem_def [code del] |
18 declare mem_def [code del] |
19 declare Collect_def [code del] |
19 declare Collect_def [code del] |
20 declare insert_code [code del] |
20 declare insert_code [code del] |