Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Quickcheck_Narrowing.thy
changeset 82773 4ec8e654112f
parent 82445 bb1f2a03b370 
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 26 17:30:33 2025 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -271,8 +271,6 @@
 
 end
 
-declare [[code drop: "partial_term_of :: int itself \<Rightarrow> _"]]
-
 lemma [code]:
   "partial_term_of (ty :: int itself) (Narrowing_variable p t) \<equiv>
     Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
@@ -293,8 +291,6 @@
 
 end
 
-declare [[code drop: "partial_term_of :: integer itself \<Rightarrow> _"]]  
-
 lemma [code]:
   "partial_term_of (ty :: integer itself) (Narrowing_variable p t) \<equiv>
     Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Code_Numeral.integer'') [])"
isabelle