# HG changeset patch
# User wenzelm
# Date 948387479 -3600
# Node ID fb6fe34060ca7074c443b90f217547c2cac7ea49
# Parent  8c65f3ca13f2cd4b9ad3ccedefaa0b939b19f6f5
removed Isar_examples/Minimal;

diff -r 8c65f3ca13f2 -r fb6fe34060ca src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Jan 18 11:33:31 2000 +0100
+++ b/src/HOL/IsaMakefile	Thu Jan 20 17:57:59 2000 +0100
@@ -420,7 +420,7 @@
   Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
   Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \
   Isar_examples/Group.thy Isar_examples/KnasterTarski.thy \
-  Isar_examples/MultisetOrder.thy Isar_examples/Minimal.thy \
+  Isar_examples/MultisetOrder.thy \
   Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
   Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
   Isar_examples/ROOT.ML Isar_examples/W_correct.thy \
diff -r 8c65f3ca13f2 -r fb6fe34060ca src/HOL/Isar_examples/Minimal.thy
--- a/src/HOL/Isar_examples/Minimal.thy	Tue Jan 18 11:33:31 2000 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-
-header {* The mimimality principle *};
-
-theory Minimal = Main:;
-
-consts
-  rel :: "'a => 'a => bool"  (infixl "<<" 50);
-axioms
-  induct: "(ALL m. m << n --> P m ==> P n) ==> P n";
-
-theorem "A ~= {} ==> EX n. n:A & (ALL m. m << n --> m ~: A)"
-  (concl is "Ex ?minimal");
-proof -;
-  assume "A ~= {}";
-  hence "EX n. n:A"; by blast;
-  thus ?thesis;
-  proof;
-    fix n; assume h: "n:A";
-    have "n:A --> Ex ?minimal" (is "?P n");
-    proof (rule induct [of n]);
-      fix m;
-      assume hyp: "ALL m. m << n --> ?P m";
-      show "?P n";
-      proof;
-	show "Ex ?minimal";
-	proof (rule case_split);
-	  assume "EX m. m << n & m:A";
-	  with hyp; show ?thesis; by blast;
-	next;
-	  assume "~ (EX m. m << n & m:A)";
-	  with h; have "?minimal n"; by blast;
-	  thus ?thesis; ..;
-	qed;
-      qed;
-    qed;
-    thus ?thesis; ..;
-  qed;
-qed;
-
-text {* \medskip Prefer a short, tactic script-style proof? *};
-
-theorem "A ~= {} ==> EX n. n:A & (ALL m. m << n --> m ~: A)";
-proof -;
-  assume "A ~= {}";
-  {{; fix n; have "n:A --> ?thesis"; by (rule induct [of n]) blast; }};
-  thus ?thesis; by (force! simp add: not_empty);
-qed;
-
-end;
diff -r 8c65f3ca13f2 -r fb6fe34060ca src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Tue Jan 18 11:33:31 2000 +0100
+++ b/src/HOL/Isar_examples/ROOT.ML	Thu Jan 20 17:57:59 2000 +0100
@@ -17,4 +17,3 @@
 with_path "../W0" time_use_thy "W_correct";
 with_path "../ex" time_use_thy "Fibonacci";
 time_use_thy "Puzzle";
-time_use_thy "Minimal";