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.
Theory.add_finals_i;
authorwenzelm
Thu, 29 Sep 2005 00:58:56 +0200
changeset 17703 6ec36bad47ea
parent 17702 ea88ddeafabe
child 17704 f776b3bf4126
Theory.add_finals_i;
src/Pure/axclass.ML file | annotate | diff | comparison | revisions
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/axclass.ML	Thu Sep 29 00:58:55 2005 +0200
+++ b/src/Pure/axclass.ML	Thu Sep 29 00:58:56 2005 +0200
@@ -218,6 +218,7 @@
     (*store info*)
     val final_thy =
       axms_thy
+      |> Theory.add_finals_i false [Const (Sign.const_of_class class, a_itselfT --> propT)]
       |> (#1 o PureThy.add_thms ((map #1 axms ~~ axioms) ~~ atts))
       |> Theory.restore_naming class_thy
       |> AxclassesData.map (Symtab.update (class, info));
--- a/src/Pure/pure_thy.ML	Thu Sep 29 00:58:55 2005 +0200
+++ b/src/Pure/pure_thy.ML	Thu Sep 29 00:58:56 2005 +0200
@@ -509,7 +509,8 @@
     [Const ("==", [aT, aT] ---> propT),
      Const ("==>", [propT, propT] ---> propT),
      Const ("all", (aT --> propT) --> propT),
-     Const ("TYPE", a_itselfT)]
+     Const ("TYPE", a_itselfT),
+     Const (Term.dummy_patternN, aT)]
   |> Theory.add_modesyntax ("", false)
     (Syntax.pure_syntax_output @ Syntax.pure_appl_syntax)
   |> Theory.add_trfuns Syntax.pure_trfuns
isabelle