# HG changeset patch
# User urbanc
# Date 1213256233 -7200
# Node ID 1ef88d06362f8b4451b857fda4d0380067e95212
# Parent  9506c7e73cfae0674dc4d191d29c710108bc6cf4
tuned header and comments

diff -r 9506c7e73cfa -r 1ef88d06362f src/HOL/Nominal/Examples/Type_Preservation.thy
--- a/src/HOL/Nominal/Examples/Type_Preservation.thy	Wed Jun 11 18:15:36 2008 +0200
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy	Thu Jun 12 09:37:13 2008 +0200
@@ -1,7 +1,17 @@
+(* $Id$ *)
+
 theory Type_Preservation
   imports Nominal
 begin
 
+text {*
+
+  This theory shows how to prove the type preservation
+  property for the simply-typed lambda-calculus and 
+  beta-reduction.
+ 
+*}
+
 atom_decl name
 
 nominal_datatype lam =
@@ -58,7 +68,7 @@
 where
   "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^isub>1 \<longrightarrow> x \<in> set \<Gamma>\<^isub>2"
 
-text {* Validity of typing contexts *}
+text {* Validity of Typing Contexts *}
 
 inductive
   valid :: "(name\<times>ty) list \<Rightarrow> bool"
@@ -92,7 +102,7 @@
 using a1 a2 a3
 by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)
 
-text {* typing relation *}
+text {* Typing Relation *}
 
 inductive
   typing :: "ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _") 
@@ -159,7 +169,7 @@
 using a b
 by (auto intro: type_substitution_aux[where \<Delta>="[]",simplified])
 
-text {* Beta reduction *}
+text {* Beta Reduction *}
 
 inductive 
   "beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _")