equal
deleted
inserted
replaced
4 |
4 |
5 header {* Abstraction Theory -- tailored for I/O automata *} |
5 header {* Abstraction Theory -- tailored for I/O automata *} |
6 |
6 |
7 theory Abstraction |
7 theory Abstraction |
8 imports LiveIOA |
8 imports LiveIOA |
9 uses ("ioa_package.ML") |
9 uses ("ioa.ML") |
10 begin |
10 begin |
11 |
11 |
12 defaultsort type |
12 defaultsort type |
13 |
13 |
14 definition |
14 definition |
611 end |
611 end |
612 *} |
612 *} |
613 |
613 |
614 method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} "" |
614 method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} "" |
615 |
615 |
616 use "ioa_package.ML" |
616 use "ioa.ML" |
617 |
617 |
618 end |
618 end |