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.
drop poisonous code equations
authorhaftmann
Sat, 07 Mar 2009 10:06:31 +0100
changeset 30332 0d07f4823d3a
parent 30331 32ccef17d408
child 30333 e9971af27b11
drop poisonous code equations
src/HOL/ex/ExecutableContent.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/ExecutableContent.thy	Sat Mar 07 10:06:12 2009 +0100
+++ b/src/HOL/ex/ExecutableContent.thy	Sat Mar 07 10:06:31 2009 +0100
@@ -24,7 +24,18 @@
   "~~/src/HOL/ex/Records"
 begin
 
-lemma [code, code del]: "(term_of \<Colon> 'a Predicate.pred \<Rightarrow> term) = term_of" ..
+lemma [code, code del]:
+  "(size :: 'a::size Predicate.pred => nat) = size" ..
+lemma [code, code del]:
+  "pred_size = pred_size" ..
+lemma [code, code del]:
+  "pred_case = pred_case" ..
+lemma [code, code del]:
+  "pred_rec = pred_rec" ..
+lemma [code, code del]:
+  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
+lemma [code, code del]:
+  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
 
 text {* However, some aren't executable *}
isabelle