equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 subsection \<open>Extracting the program\<close> |
6 subsection \<open>Extracting the program\<close> |
7 |
7 |
8 theory Higman_Extraction |
8 theory Higman_Extraction |
9 imports Higman Old_Datatype "~~/src/HOL/Library/Open_State_Syntax" |
9 imports Higman "HOL-Library.Old_Datatype" "HOL-Library.Open_State_Syntax" |
10 begin |
10 begin |
11 |
11 |
12 declare R.induct [ind_realizer] |
12 declare R.induct [ind_realizer] |
13 declare T.induct [ind_realizer] |
13 declare T.induct [ind_realizer] |
14 declare L.induct [ind_realizer] |
14 declare L.induct [ind_realizer] |