In c3ca292c1484 src/HOL/Fields.thy, there is a pseudo fact-collection
sign_simps with a comment (from about 2007):
Lemmas @{text sign_simps} is a first attempt to automate proofs
of positivity/negativity needed for @{text field_simps}. Have not added @{text
sign_simps} to @{text field_simps}
Hi all,
while reviewing some technical details of code generation, I stumbled
over a confusion in the predicate compiler regarding what a
»constructor« is supposed to be.
The presumably fundamental notions are given in predicate_compile_aux.ML
(c3ca292c1484) as:
(* check if a term
Hi Clemens,
I am struggling to reproduce the behaviour you describe. Find attached
my attempt to contrieve an example. Unfortunately, the looping is not
reproducible in c3ca292c1484. Can you provide more detail?
Thanks,
Florian
Am 12.02.2015 um 22:19 schrieb Clemens Ballarin:
Hi
On 14 February, 2015 10:11 CET, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
I guess you found out using bisection. But I read some incertainty in
your words »appears to have been introduced«. Is the changeset
8fab871a2a6f a reliable entrance point or a first
I forgot to attach the example. Loops here also for 4862f3dc9540 (12 Feb 2015).
Clemens
On 14 February, 2015 14:25 CET, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Hi Clemens,
I am struggling to reproduce the behaviour you describe. Find attached
my attempt to
This might indicate that something is wrong in the local theory stack
here, maybe the last line in
fun locale_dependency locale dep_morph mixin export =
(Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin
export
# Locale.activate_fragment_nonbrittle dep_morph
This might indicate that something is wrong in the local theory stack
here, maybe the last line in
fun locale_dependency locale dep_morph mixin export =
(Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph
mixin export
# Locale.activate_fragment_nonbrittle
I really don’t see the gain from getting rid of sign_simps, even if it is
unsuccessful. Except for the occurrence
linordered_field_class.sign_simps(41)
in Multivariate_Analysis/Derivative.thy.
Larry
On 14 Feb 2015, at 10:32, Florian Haftmann
It appears to be a reading issue.
sublocale loc1 x: loc2 A c (* sigma_1 *)
where x.b == B and x.d == e (* tau_1 *)
sorry
sublocale loc2 x: loc1 A b (* sigma_2 *)
where x.c == C and x.e == d (* tau_2 *)
sorry
Here the second mixin equation already parses as »loc1.e A ≡ loc1.e A«.
A few first traces.
The sublocale statements themselves are operative in Isabelle2013-1.
However, if put into a local context, the same situation as in
Isabelle2014 occurs:
context loc1
begin
sublocale x: loc2 A c (* sigma_1 *)
where x.b == B and x.d == e (* tau_1 *)
sorry
end
context loc2
It looks like there are more of these kinds of problems lurking, but
unfortunately, I no longer fully understand the code, so I will have to rely
on your help.
In particular, I would like to know what went wrong here.
Can you point me to a source position where you get stuck? Doing a
short
The sublocale statements themselves are operative in Isabelle2013-1.
^
This should read Isabelle2013-2, sorry for the slip.
--
PGP available:
Hi Clemens,
thanks for investigating this.
Am 12.02.2015 um 22:19 schrieb Clemens Ballarin:
Hi Florian,
I'm investigating a regression which prevents identifying certain equivalent
locales through circular sublocale declarations:
sublocale loc1 x: loc2 A c (* sigma_1 *)
where
If there are any side-conditions, important projects in the pipeline
etc. this is a good point to start discussions in a leisurely manner.
Apart from minor stuff, I plan to take care of the announced problems
for the sublocale command and case patterns in generated code.
I would appreciate if
14 matches
Mail list logo
