|
18425
|
1 |
|
|
18661
|
2 |
theory Class
|
|
18425
|
3 |
imports "../nominal"
|
|
|
4 |
begin
|
|
18395
|
5 |
|
|
|
6 |
atom_decl name coname
|
|
|
7 |
|
|
|
8 |
section {* Term-Calculus from my PHD *}
|
|
|
9 |
|
|
|
10 |
nominal_datatype trm = Ax "name" "coname"
|
|
18425
|
11 |
| ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname" ("ImpR [_].[_]._ _" [100,100,100,100] 100)
|
|
|
12 |
| ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"("ImpL [_]._ [_]._ _" [100,100,100,100,100] 100)
|
|
|
13 |
| Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" ("Cut [_]._ [_]._" [100,100,100,100] 100)
|
|
18395
|
14 |
|
|
18661
|
15 |
thm trm.induct
|
|
|
16 |
thm trm.inducts
|
|
|
17 |
thm trm.induct'
|
|
18395
|
18 |
|