src/HOL/NumberTheory/IntFact.thy

--- a/src/HOL/NumberTheory/IntFact.thy	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/NumberTheory/IntFact.thy	Fri Oct 05 21:52:39 2001 +0200
@@ -10,7 +10,7 @@
 
 text {*
   Factorial on integers and recursively defined set including all
-  Integers from @{term 2} up to @{term a}.  Plus definition of product
+  Integers from @{text 2} up to @{text a}.  Plus definition of product
   of finite set.
 
   \bigskip
@@ -22,18 +22,18 @@
   d22set :: "int => int set"
 
 recdef zfact  "measure ((\<lambda>n. nat n) :: int => nat)"
-  "zfact n = (if n \<le> #0 then #1 else n * zfact (n - #1))"
+  "zfact n = (if n \<le> Numeral0 then Numeral1 else n * zfact (n - Numeral1))"
 
 defs
-  setprod_def: "setprod A == (if finite A then fold (op *) #1 A else #1)"
+  setprod_def: "setprod A == (if finite A then fold (op *) Numeral1 A else Numeral1)"
 
 recdef d22set  "measure ((\<lambda>a. nat a) :: int => nat)"
-  "d22set a = (if #1 < a then insert a (d22set (a - #1)) else {})"
+  "d22set a = (if Numeral1 < a then insert a (d22set (a - Numeral1)) else {})"
 
 
 text {* \medskip @{term setprod} --- product of finite set *}
 
-lemma setprod_empty [simp]: "setprod {} = #1"
+lemma setprod_empty [simp]: "setprod {} = Numeral1"
   apply (simp add: setprod_def)
   done
 
@@ -46,7 +46,7 @@
 
 text {*
   \medskip @{term d22set} --- recursively defined set including all
-  integers from @{term 2} up to @{term a}
+  integers from @{text 2} up to @{text a}
 *}
 
 declare d22set.simps [simp del]
@@ -54,7 +54,7 @@
 
 lemma d22set_induct:
   "(!!a. P {} a) ==>
-    (!!a. #1 < (a::int) ==> P (d22set (a - #1)) (a - #1)
+    (!!a. Numeral1 < (a::int) ==> P (d22set (a - Numeral1)) (a - Numeral1)
       ==> P (d22set a) a)
     ==> P (d22set u) u"
 proof -
@@ -62,14 +62,14 @@
   show ?thesis
     apply (rule d22set.induct)
     apply safe
-     apply (case_tac [2] "#1 < a")
+     apply (case_tac [2] "Numeral1 < a")
       apply (rule_tac [2] rule_context)
        apply (simp_all (no_asm_simp))
      apply (simp_all (no_asm_simp) add: d22set.simps rule_context)
     done
 qed
 
-lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> #1 < b"
+lemma d22set_g_1 [rule_format]: "b \<in> d22set a --> Numeral1 < b"
   apply (induct a rule: d22set_induct)
    prefer 2
    apply (subst d22set.simps)
@@ -87,7 +87,7 @@
   apply (auto dest: d22set_le)
   done
 
-lemma d22set_mem [rule_format]: "#1 < b --> b \<le> a --> b \<in> d22set a"
+lemma d22set_mem [rule_format]: "Numeral1 < b --> b \<le> a --> b \<in> d22set a"
   apply (induct a rule: d22set.induct)
   apply auto
    apply (simp_all add: d22set.simps)
@@ -109,7 +109,7 @@
    apply (simp add: d22set.simps zfact.simps)
   apply (subst d22set.simps)
   apply (subst zfact.simps)
-  apply (case_tac "#1 < a")
+  apply (case_tac "Numeral1 < a")
    prefer 2
    apply (simp add: d22set.simps zfact.simps)
   apply (simp add: d22set_fin d22set_le_swap)