| changeset 20955 | 65a9a30b8ece |
| parent 20606 | fd9b0b78a7d3 |
| child 21087 | 3e56528a39f7 |
--- a/src/HOL/Nominal/Examples/Compile.thy Tue Oct 10 15:33:25 2006 +0200 +++ b/src/HOL/Nominal/Examples/Compile.thy Tue Oct 10 16:26:59 2006 +0200 @@ -54,7 +54,7 @@ inductive ctxts intros v1[intro]: "valid []" -v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" +v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" (* maybe dom of \<Gamma> *) text {* typing judgements for trms *}