# HG changeset patch
# User wenzelm
# Date 1330381838 -3600
# Node ID d0491ab69c84bd61353ea42782a90d7ec79e81e0
# Parent  f88b187ad8caa314338432fd74cd6b80c7f52b6b
removed dead code (cf. a34d89ce6097);

diff -r f88b187ad8ca -r d0491ab69c84 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Feb 27 21:07:00 2012 +0100
+++ b/src/HOL/IsaMakefile	Mon Feb 27 23:30:38 2012 +0100
@@ -963,11 +963,10 @@
 
 HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
 
-$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL					\
-  MicroJava/ROOT.ML MicroJava/Comp/AuxLemmas.thy			\
-  MicroJava/Comp/CorrComp.thy MicroJava/Comp/CorrCompTp.thy		\
-  MicroJava/Comp/DefsComp.thy MicroJava/Comp/Index.thy			\
-  MicroJava/Comp/LemmasComp.thy MicroJava/Comp/NatCanonify.thy		\
+$(LOG)/HOL-MicroJava.gz: $(OUT)/HOL MicroJava/ROOT.ML			\
+  MicroJava/Comp/AuxLemmas.thy MicroJava/Comp/CorrComp.thy		\
+  MicroJava/Comp/CorrCompTp.thy MicroJava/Comp/DefsComp.thy		\
+  MicroJava/Comp/Index.thy MicroJava/Comp/LemmasComp.thy		\
   MicroJava/Comp/TranslComp.thy MicroJava/Comp/TranslCompTp.thy		\
   MicroJava/Comp/TypeInf.thy MicroJava/J/Conform.thy			\
   MicroJava/J/Eval.thy MicroJava/J/JBasis.thy				\
@@ -984,7 +983,8 @@
   MicroJava/DFA/LBVSpec.thy MicroJava/DFA/Listn.thy			\
   MicroJava/DFA/Opt.thy MicroJava/DFA/Product.thy			\
   MicroJava/DFA/SemilatAlg.thy MicroJava/DFA/Semilat.thy		\
-  MicroJava/DFA/Semilattices.thy MicroJava/DFA/Typing_Framework_err.thy	\
+  MicroJava/DFA/Semilattices.thy					\
+  MicroJava/DFA/Typing_Framework_err.thy				\
   MicroJava/DFA/Typing_Framework.thy MicroJava/BV/BVSpec.thy		\
   MicroJava/BV/BVSpecTypeSafe.thy MicroJava/BV/Correct.thy		\
   MicroJava/BV/JType.thy MicroJava/BV/JVM.thy MicroJava/BV/JVMType.thy	\
diff -r f88b187ad8ca -r d0491ab69c84 src/HOL/MicroJava/Comp/NatCanonify.thy
--- a/src/HOL/MicroJava/Comp/NatCanonify.thy	Mon Feb 27 21:07:00 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(*  Title:      HOL/MicroJava/Comp/NatCanonify.thy
-    Author:     Martin Strecker
-*)
-
-theory NatCanonify imports Main begin
-
-(************************************************************************)
-  (* Canonizer for converting nat to int *)
-(************************************************************************)
-
-lemma nat_add_canonify: "(n1::nat) + n2 = nat ((int n1) + (int n2))"
-by (simp add: nat_add_distrib)
-
-lemma nat_mult_canonify: "(n1::nat) * n2 = nat ((int n1) * (int n2))"
-by (simp add: nat_mult_distrib)
-
-lemma nat_diff_canonify: "(n1::nat) - n2 = 
-  nat (if (int n1) \<le> (int n2) then 0 else (int n1) - (int n2))"
-by (simp add: zdiff_int nat_int)
-
-lemma nat_le_canonify: "((n1::nat) \<le> n2) = ((int n1) \<le> (int n2))"
-by arith
-
-lemma nat_less_canonify: "((n1::nat) < n2) = ((int n1) < (int n2))"
-by arith
-
-lemma nat_eq_canonify: "((n1::nat) = n2) = ((int n1) = (int n2))"
-by arith
-
-lemma nat_if_canonify: "(if b then (n1::nat) else n2) =
-  nat (if b then (int n1) else (int n2))"
-by simp
-
-lemma int_nat_canonify: "(int (nat n)) = (if 0 \<le> n then n else 0)"
-by simp
-
-lemmas nat_canonify = 
-  nat_add_canonify nat_mult_canonify nat_diff_canonify 
-  nat_le_canonify nat_less_canonify nat_eq_canonify nat_if_canonify 
-  int_nat_canonify nat_int
-
-end