src/FOLP/ex/Nat.ML
 changeset 17480 fd19f77dcf60 parent 5061 f947332d5465 child 24584 01e83ffa6c54
```     1.1 --- a/src/FOLP/ex/Nat.ML	Sat Sep 17 20:49:14 2005 +0200
1.2 +++ b/src/FOLP/ex/Nat.ML	Sun Sep 18 14:25:48 2005 +0200
1.3 @@ -2,17 +2,8 @@
1.4      ID:         \$Id\$
1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.6      Copyright   1992  University of Cambridge
1.7 -
1.8 -Examples for the manual "Introduction to Isabelle"
1.9 -
1.10 -Proofs about the natural numbers
1.11 -
1.12 -To generate similar output to manual, execute these commands:
1.13 -    Pretty.setmargin 72; print_depth 0;
1.14  *)
1.15
1.16 -open Nat;
1.17 -
1.18  Goal "?p : ~ (Suc(k) = k)";
1.19  by (res_inst_tac [("n","k")] induct 1);
1.20  by (rtac notI 1);
1.21 @@ -42,23 +33,23 @@
1.23
1.24  (*
1.25 -val nat_congs = mk_congs Nat.thy ["Suc", "op +"];
1.26 +val nat_congs = mk_congs (the_context ()) ["Suc", "op +"];
1.27  prths nat_congs;
1.28  *)
1.29 -val prems = goal Nat.thy "p: x=y ==> ?p : Suc(x) = Suc(y)";
1.30 +val prems = goal (the_context ()) "p: x=y ==> ?p : Suc(x) = Suc(y)";
1.31  by (resolve_tac (prems RL [subst]) 1);
1.32  by (rtac refl 1);
1.33  val Suc_cong = result();
1.34
1.35 -val prems = goal Nat.thy "[| p : a=x;  q: b=y |] ==> ?p : a+b=x+y";
1.36 -by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN
1.37 +val prems = goal (the_context ()) "[| p : a=x;  q: b=y |] ==> ?p : a+b=x+y";
1.38 +by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN
1.39      rtac refl 1);
1.40  val Plus_cong = result();
1.41
1.42  val nat_congs = [Suc_cong,Plus_cong];
1.43
1.44