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.
renamed split_T_case_prem to split_T_case_asm
authoroheimb
Wed, 12 Nov 1997 12:24:55 +0100
changeset 4204 7b15e7eee982
parent 4203 ca73de799b73
child 4205 96632970d203
renamed split_T_case_prem to split_T_case_asm
src/HOL/thy_syntax.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/thy_syntax.ML	Wed Nov 12 12:23:37 1997 +0100
+++ b/src/HOL/thy_syntax.ML	Wed Nov 12 12:24:55 1997 +0100
@@ -165,7 +165,7 @@
     \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
       ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
     \            ALLGOALS Asm_simp_tac]);\n\
-    \val split_"^tname^"_case_prem = prove_goal thy (#2(split_"^tname^"_eqns))\n\
+    \val split_"^tname^"_case_asm = prove_goal thy (#2(split_"^tname^"_eqns))\n\
     \  (fn _ => [#exhaust_tac (datatype_info thy (Sign.intern_tycon (sign_of thy) "
       ^ quote tname ^ ")) \""^tname^"0\" 1,\n\
     \            ALLGOALS Asm_simp_tac]);\n\
isabelle