# HG changeset patch # User haftmann # Date 1175264342 -7200 # Node ID b860975e47b493c849baee928741f7b773c8403c # Parent 70f5cf8a0fadac11c438f4c98abb34fee32272bb tuned diff -r 70f5cf8a0fad -r b860975e47b4 src/HOL/Library/Pure_term.thy --- a/src/HOL/Library/Pure_term.thy Fri Mar 30 16:19:01 2007 +0200 +++ b/src/HOL/Library/Pure_term.thy Fri Mar 30 16:19:02 2007 +0200 @@ -67,6 +67,11 @@ subsection {* Code generator setup *} +lemma [code func]: + "tyco1 {\} tys1 = tyco2 {\} tys2 \ tyco1 = tyco2 + \ list_all2 (op =) tys1 tys2" + by (auto simp add: list_all2_eq [symmetric]) + definition Bound :: "int \ term" where @@ -107,9 +112,19 @@ and "Term.Abs/ (_, _, _)" and "Term.Bound/ (IntInf.toInt/ _)") code_const term_rec and term_case and "size \ term \ nat" + and "op = \ term \ term \ bool" (SML "!(_; _; _; _; _; raise Fail \"term'_rec\")" and "!(_; _; _; _; _; raise Fail \"term'_case\")" - and "!(_; raise Fail \"size'_term\")") + and "!(_; raise Fail \"size'_term\")" + and "!(_; _; raise Fail \"eq'_term\")") + (OCaml "!(_; _; _; _; _; failwith \"term'_rec\")" + and "!(_; _; _; _; _; failwith \"term'_case\")" + and "!(_; failwith \"size'_term\")" + and "!(_; _; failwith \"eq'_term\")") + (Haskell "error/ \"term'_rec\"" + and "error/ \"term'_case\"" + and "error/ \"size'_term\"" + and "error/ \"eq'_term\"") code_reserved SML Term diff -r 70f5cf8a0fad -r b860975e47b4 src/HOL/ex/ExecutableContent.thy --- a/src/HOL/ex/ExecutableContent.thy Fri Mar 30 16:19:01 2007 +0200 +++ b/src/HOL/ex/ExecutableContent.thy Fri Mar 30 16:19:02 2007 +0200 @@ -1,3 +1,4 @@ + (* ID: $Id$ Author: Florian Haftmann, TU Muenchen *)