equal
deleted
inserted
replaced
7 theory BVExample |
7 theory BVExample |
8 imports |
8 imports |
9 "../JVM/JVMListExample" |
9 "../JVM/JVMListExample" |
10 BVSpecTypeSafe |
10 BVSpecTypeSafe |
11 JVM |
11 JVM |
12 "~~/src/HOL/Library/Executable_Set" |
12 "~~/src/HOL/Library/More_Set" |
13 begin |
13 begin |
14 |
14 |
15 text {* |
15 text {* |
16 This theory shows type correctness of the example program in section |
16 This theory shows type correctness of the example program in section |
17 \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by |
17 \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by |
435 |
435 |
436 definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]: |
436 definition some_elem :: "'a set \<Rightarrow> 'a" where [code del]: |
437 "some_elem = (%S. SOME x. x : S)" |
437 "some_elem = (%S. SOME x. x : S)" |
438 code_const some_elem |
438 code_const some_elem |
439 (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)") |
439 (SML "(case/ _ of/ Set/ xs/ =>/ hd/ xs)") |
440 setup {* Code.add_signature_cmd ("some_elem", "'a set \<Rightarrow> 'a") *} |
|
441 |
440 |
442 text {* This code setup is just a demonstration and \emph{not} sound! *} |
441 text {* This code setup is just a demonstration and \emph{not} sound! *} |
443 |
442 |
444 lemma False |
443 lemma False |
445 proof - |
444 proof - |