Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
cleaned comment;
authorwenzelm
Thu, 09 Mar 2000 22:56:40 +0100
changeset 8400 64921d1fef15
parent 8399 86b04d47b853
child 8401 50d5f4402305
cleaned comment;
src/HOL/Tools/induct_method.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/rule_cases.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/induct_method.ML	Thu Mar 09 18:27:18 2000 +0100
+++ b/src/HOL/Tools/induct_method.ML	Thu Mar 09 22:56:40 2000 +0100
@@ -213,7 +213,7 @@
 
     val rules =
       (case (args, facts) of
-        ((None, None), []) => [RuleCases.none case_split_thm]
+        ((None, None), []) => [RuleCases.none case_split_thm]		(* FIXME add cases!? *)
       | ((Some t, None), []) =>
           let val name = type_name t in
             (case lookup_casesT ctxt name of
--- a/src/Pure/Isar/rule_cases.ML	Thu Mar 09 18:27:18 2000 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Mar 09 22:56:40 2000 +0100
@@ -3,9 +3,6 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Manage local contexts of rules.
-
-TODO:
-  - instantiation of cases (including type vars!);
 *)
 
 signature RULE_CASES =
isabelle