--- 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 \
--- 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;
--- 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";