# HG changeset patch
# User wenzelm
# Date 1201455152 -3600
# Node ID 89a03048f312b7e41b12fb3f0cca5b0ffcda326c
# Parent  bfda3f3beccd1317822b8c667b5d61ac41167f10
removed legacy ML file;

diff -r bfda3f3beccd -r 89a03048f312 doc-src/AxClass/IsaMakefile
--- a/doc-src/AxClass/IsaMakefile	Sat Jan 26 23:15:33 2008 +0100
+++ b/doc-src/AxClass/IsaMakefile	Sun Jan 27 18:32:32 2008 +0100
@@ -36,7 +36,7 @@
 FOL:
 	@cd $(SRC)/FOL; $(ISATOOL) make FOL
 
-$(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/NatClass.ML Nat/NatClass.thy
+$(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/NatClass.thy
 	@$(USEDIR) $(OUT)/FOL Nat
 	@rm -f Nat/document/*.sty Nat/document/session.tex
 
diff -r bfda3f3beccd -r 89a03048f312 doc-src/AxClass/Nat/NatClass.ML
--- a/doc-src/AxClass/Nat/NatClass.ML	Sat Jan 26 23:15:33 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-(*  Title:      Doc/AxClass/Nat/NatClass.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-This is Nat.ML with some trivial modifications in order to make it
-work with NatClass.thy.
-*)
-
-val induct = thm "induct";
-val Suc_inject = thm "Suc_inject";
-val Suc_neq_0 = thm "Suc_neq_0";
-val rec_0 = thm "rec_0";
-val rec_Suc = thm "rec_Suc";
-val add_def = thm "add_def";
-
-
-Goal "Suc(k) ~= (k::'a::nat)";
-by (res_inst_tac [("n","k")] induct 1);
-by (rtac notI 1);
-by (etac Suc_neq_0 1);
-by (rtac notI 1);
-by (etac notE 1);
-by (etac Suc_inject 1);
-qed "Suc_n_not_n";
-
-
-Goal "(k+m)+n = k+(m+n)";
-prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
-by (rtac induct 1);
-back();
-back();
-back();
-back();
-back();
-back();
-
-Goalw [add_def] "\<zero>+n = n";
-by (rtac rec_0 1);
-qed "add_0";
-
-Goalw [add_def] "Suc(m)+n = Suc(m+n)";
-by (rtac rec_Suc 1);
-qed "add_Suc";
-
-Addsimps [add_0, add_Suc];
-
-Goal "(k+m)+n = k+(m+n)";
-by (res_inst_tac [("n","k")] induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_assoc";
-
-Goal "m+\<zero> = m";
-by (res_inst_tac [("n","m")] induct 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-qed "add_0_right";
-
-Goal "m+Suc(n) = Suc(m+n)";
-by (res_inst_tac [("n","m")] induct 1);
-by (ALLGOALS (Asm_simp_tac));
-qed "add_Suc_right";
-
-val [prem] = Goal "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
-by (res_inst_tac [("n","i")] induct 1);
-by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [prem]) 1);
-qed "";
-
diff -r bfda3f3beccd -r 89a03048f312 doc-src/AxClass/Nat/NatClass.thy
--- a/doc-src/AxClass/Nat/NatClass.thy	Sat Jan 26 23:15:33 2008 +0100
+++ b/doc-src/AxClass/Nat/NatClass.thy	Sun Jan 27 18:32:32 2008 +0100
@@ -58,4 +58,60 @@
  constraints).
 *}
 
+(*<*)
+lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)"
+apply (rule_tac n = k in induct)
+apply (rule notI)
+apply (erule Suc_neq_0)
+apply (rule notI)
+apply (erule notE)
+apply (erule Suc_inject)
+done
+
+lemma "(k+m)+n = k+(m+n)"
+apply (rule induct)
+back
+back
+back
+back
+back
+back
+oops
+
+lemma add_0 [simp]: "\<zero>+n = n"
+apply (unfold add_def)
+apply (rule rec_0)
+done
+
+lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)"
+apply (unfold add_def)
+apply (rule rec_Suc)
+done
+
+lemma add_assoc: "(k+m)+n = k+(m+n)"
+apply (rule_tac n = k in induct)
+apply simp
+apply simp
+done
+
+lemma add_0_right: "m+\<zero> = m"
+apply (rule_tac n = m in induct)
+apply simp
+apply simp
+done
+
+lemma add_Suc_right: "m+Suc(n) = Suc(m+n)"
+apply (rule_tac n = m in induct)
+apply simp_all
+done
+
+lemma
+  assumes prem: "!!n. f(Suc(n)) = Suc(f(n))"
+  shows "f(i+j) = i+f(j)"
+apply (rule_tac n = i in induct)
+apply simp
+apply (simp add: prem)
+done
+(*>*)
+
 end
\ No newline at end of file
diff -r bfda3f3beccd -r 89a03048f312 doc-src/AxClass/Nat/document/NatClass.tex
--- a/doc-src/AxClass/Nat/document/NatClass.tex	Sat Jan 26 23:15:33 2008 +0100
+++ b/doc-src/AxClass/Nat/document/NatClass.tex	Sun Jan 27 18:32:32 2008 +0100
@@ -76,6 +76,111 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+%
 \isadelimtheory
 %
 \endisadelimtheory