equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 section \<open>Language of a Grammar\<close> |
8 section \<open>Language of a Grammar\<close> |
9 |
9 |
10 theory Gram_Lang |
10 theory Gram_Lang |
11 imports DTree "~~/src/HOL/Library/Infinite_Set" |
11 imports DTree "HOL-Library.Infinite_Set" |
12 begin |
12 begin |
13 |
13 |
14 |
14 |
15 (* We assume that the sets of terminals, and the left-hand sides of |
15 (* We assume that the sets of terminals, and the left-hand sides of |
16 productions are finite and that the grammar has no unused nonterminals. *) |
16 productions are finite and that the grammar has no unused nonterminals. *) |