src/HOL/Lambda/InductTermi.thy
changeset 25972 94b15338da8d
parent 23750 a1db5f819d00
child 26806 40b411ec05aa
     1.1 --- a/src/HOL/Lambda/InductTermi.thy	Fri Jan 25 22:04:46 2008 +0100
     1.2 +++ b/src/HOL/Lambda/InductTermi.thy	Fri Jan 25 23:05:23 2008 +0100
     1.3 @@ -21,7 +21,7 @@
     1.4    | Beta [intro]: "IT ((r[s/0]) \<degree>\<degree> ss) ==> IT s ==> IT ((Abs r \<degree> s) \<degree>\<degree> ss)"
     1.5  
     1.6  
     1.7 -subsection {* Every term in IT terminates *}
     1.8 +subsection {* Every term in @{text "IT"} terminates *}
     1.9  
    1.10  lemma double_induction_lemma [rule_format]:
    1.11    "termip beta s ==> \<forall>t. termip beta t -->
    1.12 @@ -56,7 +56,7 @@
    1.13    done
    1.14  
    1.15  
    1.16 -subsection {* Every terminating term is in IT *}
    1.17 +subsection {* Every terminating term is in @{text "IT"} *}
    1.18  
    1.19  declare Var_apps_neq_Abs_apps [symmetric, simp]
    1.20