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.
proper header;
authorwenzelm
Thu, 05 Nov 2009 14:47:27 +0100
changeset 33440 181fae134b43
parent 33439 f5d95787224f
child 33441 99a5f22a967d
child 33473 3b275a0bf18c
proper header; eliminated SML97's opaque signature constrain, which is essentially a legacy feature (due to problems with ML toplevel pretty printing);
src/HOLCF/Tools/adm_tac.ML file | annotate | diff | comparison | revisions 
--- a/src/HOLCF/Tools/adm_tac.ML	Thu Nov 05 14:37:39 2009 +0100
+++ b/src/HOLCF/Tools/adm_tac.ML	Thu Nov 05 14:47:27 2009 +0100
@@ -1,4 +1,5 @@
-(*  Author:     Stefan Berghofer, TU Muenchen
+(*  Title:      HOLCF/Tools/adm_tac.ML
+    Author:     Stefan Berghofer, TU Muenchen
 
 Admissibility tactic.
 
@@ -18,7 +19,7 @@
   val adm_tac: Proof.context -> (int -> tactic) -> int -> tactic
 end;
 
-structure Adm :> ADM =
+structure Adm : ADM =
 struct
isabelle