Hi!
It seems that the compilation of IsarRef is broken. I've got the
following error with the 45669:06e259492f6b changeset:
~/tmp/isabelle-dev/doc-src/IsarRef> ../../bin/isabelle make
Running HOL-IsarRef ...
HOL-IsarRef FAILED
val CONTEXT_REWRITE_RULE :
term * term list * thm * thm list -> thm -> thm * term list
val CONJUNCTS : thm -> thm list val CONJUNCT2 : thm -> thm
val CONJUNCT1 : thm -> thm val CHOOSE : cterm * thm -> thm -> thm
val ASSUME : cterm -> thm end
Loading theory "Misc"
### Introduced fixed type variable(s): 'a in "B" or "x__"
### Introduced fixed type variable(s): 'a in "a"
### Introduced fixed type variable(s): 'a in "A" or "x__"
### Introduced fixed type variable(s): 'a in "A"
### Introduced fixed type variable(s): 'a in "A" or "x__"
*** Theory loader: failed to load "HOL_Specific" (unresolved "Old_Recdef")
*** Error (line 786 of "~~/src/HOL/Tools/TFL/rules.ML"):
*** Value or constructor (add_eqcong) has not been declared in structure
Simplifier
***
*** At command "use" (line 70 of "~~/src/HOL/Library/Old_Recdef.thy")
val it = (): unit
Exception- TOPLEVEL_ERROR raised
*** ML error
make: ***
[~/.isabelle//heaps/polyml-5.4.0_x86_64-linux/log/HOL-IsarRef.gz] Error 1
Any ideas what's wrong?
Ondrej
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
