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/Complex/ex/ReflectedFerrack.thy
changeset 24348 c708ea5b109a
parent 24336 fff40259f336
child 24423 ae9cd0e92423 
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 20 18:07:31 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 20 18:07:49 2007 +0200
@@ -1986,7 +1986,7 @@
   "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
 
-code_gen linrqe ferrack_test in SML module_name Ferrack
+export_code linrqe ferrack_test in SML module_name Ferrack
 
 (*code_module Ferrack
   contains
isabelle