# HG changeset patch
# User wenzelm
# Date 1125934697 -7200
# Node ID df7c3b1f390a25f4eb710bebb3634f09565818c8
# Parent  dda237f1d299e449bbb1c5db1b39ab0371e49d6b
tuned;

diff -r dda237f1d299 -r df7c3b1f390a src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Mon Sep 05 17:38:15 2005 +0200
+++ b/src/Cube/Cube.thy	Mon Sep 05 17:38:17 2005 +0200
@@ -36,10 +36,10 @@
   arrow         :: "[term, term] => term"               (infixr "->" 10)
 
 translations
-  ("prop") "x:X"  == ("prop") "|- x:X"
-  "Lam x:A. B"  == "Abs(A, %x. B)"
-  "Pi x:A. B"   => "Prod(A, %x. B)"
-  "A -> B"      => "Prod(A, _K(B))"
+  ("prop") "x:X" == ("prop") "|- x:X"
+  "Lam x:A. B"   == "Abs(A, %x. B)"
+  "Pi x:A. B"    => "Prod(A, %x. B)"
+  "A -> B"       => "Prod(A, _K(B))"
 
 syntax (xsymbols)
   Trueprop      :: "[context_, typing_] => prop"        ("(_/ \<turnstile> _)")
@@ -84,6 +84,7 @@
 
 lemmas (in L2) rules = simple lam_bs pi_bs
 
+
 locale Lomega =
   assumes
     pi_bb: "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"
@@ -100,18 +101,22 @@
 
 lemmas (in LP) rules = simple lam_sb pi_sb
 
+
 locale LP2 = LP + L2
 
 lemmas (in LP2) rules = simple lam_bs pi_bs lam_sb pi_sb
 
+
 locale Lomega2 = L2 + Lomega
 
 lemmas (in Lomega2) rules = simple lam_bs pi_bs lam_bb pi_bb
 
+
 locale LPomega = LP + Lomega
 
 lemmas (in LPomega) rules = simple lam_bb pi_bb lam_sb pi_sb
 
+
 locale CC = L2 + LP + Lomega
 
 lemmas (in CC) rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
diff -r dda237f1d299 -r df7c3b1f390a src/Cube/ex/ROOT.ML
--- a/src/Cube/ex/ROOT.ML	Mon Sep 05 17:38:15 2005 +0200
+++ b/src/Cube/ex/ROOT.ML	Mon Sep 05 17:38:17 2005 +0200
@@ -1,2 +1,4 @@
+
+(* $Id$ *)
 
 time_use_thy "ex";
diff -r dda237f1d299 -r df7c3b1f390a src/Cube/ex/ex.thy
--- a/src/Cube/ex/ex.thy	Mon Sep 05 17:38:15 2005 +0200
+++ b/src/Cube/ex/ex.thy	Mon Sep 05 17:38:17 2005 +0200
@@ -1,3 +1,7 @@
+
+(* $Id$ *)
+
+header {* Lambda Cube Examples *}
 
 theory ex
 imports Cube
diff -r dda237f1d299 -r df7c3b1f390a src/FOL/ex/NatClass.ML
--- a/src/FOL/ex/NatClass.ML	Mon Sep 05 17:38:15 2005 +0200
+++ b/src/FOL/ex/NatClass.ML	Mon Sep 05 17:38:17 2005 +0200
@@ -6,7 +6,7 @@
 *)
 
 Goal "Suc(k) ~= (k::'a::nat)";
-by (res_inst_tac [("n","k")] induct 1);
+by (res_inst_tac [("n","k")] nat.induct 1);
 by (rtac notI 1);
 by (etac Suc_neq_0 1);
 by (rtac notI 1);
@@ -16,8 +16,8 @@
 
 
 Goal "(k+m)+n = k+(m+n)";
-prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
-by (rtac induct 1);
+prths ([nat.induct] RL [topthm()]);  (*prints all 14 next states!*)
+by (rtac nat.induct 1);
 back();
 back();
 back();
@@ -36,24 +36,24 @@
 Addsimps [add_0, add_Suc];
 
 Goal "(k+m)+n = k+(m+n)";
-by (res_inst_tac [("n","k")] induct 1);
+by (res_inst_tac [("n","k")] nat.induct 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "add_assoc";
 
 Goal "m+0 = m";
-by (res_inst_tac [("n","m")] induct 1);
+by (res_inst_tac [("n","m")] nat.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 (res_inst_tac [("n","m")] nat.induct 1);
 by (ALLGOALS (Asm_simp_tac));
 qed "add_Suc_right";
 
 val [prem] = goal (the_context ()) "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
-by (res_inst_tac [("n","i")] induct 1);
+by (res_inst_tac [("n","i")] nat.induct 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [prem]) 1);
 result();
diff -r dda237f1d299 -r df7c3b1f390a src/HOL/Real/HahnBanach/ROOT.ML
--- a/src/HOL/Real/HahnBanach/ROOT.ML	Mon Sep 05 17:38:15 2005 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML	Mon Sep 05 17:38:17 2005 +0200
@@ -5,4 +5,4 @@
 The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
 *)
 
-with_path "../../Hyperreal" time_use_thy "HahnBanach";
+time_use_thy "HahnBanach";