# HG changeset patch
# User haftmann
# Date 1272645291 -7200
# Node ID 16736dde54c0edfd5ec1ac8079d6e1190bc02094
# Parent  663bb2bc1e72de930e15131eeb414f7bf8603a83
do not generate code per default -- touches file of parent session

diff -r 663bb2bc1e72 -r 16736dde54c0 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Fri Apr 30 17:53:49 2010 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Fri Apr 30 18:34:51 2010 +0200
@@ -1909,9 +1909,11 @@
 
 ML {* @{code cooper_test} () *}
 
+(*
 code_reflect Generated_Cooper
   functions pa
   file "~~/src/HOL/Tools/Qelim/generated_cooper.ML"
+*)
 
 oracle linzqe_oracle = {*
 let