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.
tuned IsarThy.theorem_i;
authorwenzelm
Mon, 13 Nov 2000 21:59:49 +0100
changeset 10463 474263d29057
parent 10462 adf901eb9c40
child 10464 b7b916a82dca
tuned IsarThy.theorem_i;
src/HOL/Tools/typedef_package.ML file | annotate | diff | comparison | revisions
src/Pure/axclass.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/typedef_package.ML	Mon Nov 13 10:34:32 2000 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Mon Nov 13 21:59:49 2000 +0100
@@ -239,7 +239,7 @@
     val goal_pat = Thm.term_of (goal_nonempty true cset_pat);
   in
     thy
-    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef],
+    |> IsarThy.theorem_i ((("", [typedef_attribute cset do_typedef]),
       (goal, ([goal_pat], []))), comment) int
   end;
 
--- a/src/Pure/axclass.ML	Mon Nov 13 10:34:32 2000 +0100
+++ b/src/Pure/axclass.ML	Mon Nov 13 21:59:49 2000 +0100
@@ -439,7 +439,7 @@
 
 fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
   thy
-  |> IsarThy.theorem_i (("", [inst_attribute add_thms],
+  |> IsarThy.theorem_i ((("", [inst_attribute add_thms]),
     (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
 
 val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;
isabelle