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.
Added meta_spec to extraction_expand.
authorberghofe
Wed, 07 Feb 2007 18:07:10 +0100
changeset 22281 23e0fde84cb7
parent 22280 a20a203c8f41
child 22282 71b4aefad227
Added meta_spec to extraction_expand.
src/HOL/Extraction.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Extraction.thy	Wed Feb 07 18:04:44 2007 +0100
+++ b/src/HOL/Extraction.thy	Wed Feb 07 18:07:10 2007 +0100
@@ -49,7 +49,7 @@
 *}
 
 lemmas [extraction_expand] =
-  atomize_eq atomize_all atomize_imp atomize_conj
+  meta_spec atomize_eq atomize_all atomize_imp atomize_conj
   allE rev_mp conjE Eq_TrueI Eq_FalseI eqTrueI eqTrueE eq_cong2
   notE' impE' impE iffE imp_cong simp_thms eq_True eq_False
   induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
isabelle