Mercurial Mercurial > repos > isabelle / file revision
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/Codegenerator_Test/RBT_Set_Test.thy
author wenzelm
Mon, 11 Feb 2013 14:39:04 +0100
changeset 51085 d90218288d51
parent 49948 744934b818c7
child 50996 51ad7b4ac096
permissions -rw-r--r--
make WWW_Find work again, now that its ML modules reside within a theory context (cf. bf5b45870110) -- patch by Rafal Kolanski;

(*  Title:      HOL/Codegenerator_Test/RBT_Set_Test.thy
    Author:     Ondrej Kuncar
*)

header {* Test of the code generator using an implementation of sets by RBT trees *}

theory RBT_Set_Test
imports "~~/src/HOL/Library/Library" "~~/src/HOL/Library/RBT_Set"
begin

(* 
   The following code equations have to be deleted because they use 
   lists to implement sets in the code generetor. 
*)

lemma [code, code del]:
  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..

lemma [code, code del]:
  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..

lemma [code, code del]:
  "pred_of_set = pred_of_set" ..


lemma [code, code del]:
  "Cardinality.card' = Cardinality.card'" ..

lemma [code, code del]:
  "Cardinality.finite' = Cardinality.finite'" ..

lemma [code, code del]:
  "Cardinality.subset' = Cardinality.subset'" ..

lemma [code, code del]:
  "Cardinality.eq_set = Cardinality.eq_set" ..


lemma [code, code del]:
  "acc = acc" ..

(*
  If the code generation ends with an exception with the following message:
  '"List.set" is not a constructor, on left hand side of equation: ...',
  the code equation in question has to be either deleted (like many others in this file) 
  or implemented for RBT trees.
*)

export_code _ checking SML OCaml? Haskell? Scala?

end
isabelle