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.
get_thm;
authorwenzelm
Thu, 21 Oct 1999 18:46:33 +0200
changeset 7906 0576dad973b1
parent 7905 c5f735f7428c
child 7907 258f136864db
get_thm;
TFL/tfl.sml file | annotate | diff | comparison | revisions
src/HOLCF/domain/theorems.ML file | annotate | diff | comparison | revisions 
--- a/TFL/tfl.sml	Thu Oct 21 18:45:55 1999 +0200
+++ b/TFL/tfl.sml	Thu Oct 21 18:46:33 1999 +0200
@@ -538,7 +538,7 @@
        thy
        |> PureThy.add_defs_i 
             [Thm.no_attributes (fid ^ "_def", defn)]
-     val def = freezeT (get_axiom theory (fid ^ "_def"))
+     val def = freezeT (get_thm theory (fid ^ "_def"))
      val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
 	                   else ()
      (* val fconst = #lhs(S.dest_eq(concl def))  *)
--- a/src/HOLCF/domain/theorems.ML	Thu Oct 21 18:45:55 1999 +0200
+++ b/src/HOLCF/domain/theorems.ML	Thu Oct 21 18:46:33 1999 +0200
@@ -75,7 +75,7 @@
 
 (* ----- getting the axioms and definitions --------------------------------- *)
 
-local fun ga s dn = get_axiom thy (dn^"."^s) in
+local fun ga s dn = get_thm thy (dn^"."^s) in
 val ax_abs_iso    = ga "abs_iso"  dname;
 val ax_rep_iso    = ga "rep_iso"  dname;
 val ax_when_def   = ga "when_def" dname;
@@ -350,7 +350,7 @@
 
 (* ----- getting the composite axiom and definitions ------------------------ *)
 
-local fun ga s dn = get_axiom thy (dn^"."^s) in
+local fun ga s dn = get_thm thy (dn^"."^s) in
 val axs_reach      = map (ga "reach"     ) dnames;
 val axs_take_def   = map (ga "take_def"  ) dnames;
 val axs_finite_def = map (ga "finite_def") dnames;
isabelle