Walther Neuper <wneuper@ist.tugraz.at> [Mon, 07 Dec 2015 15:37:09 +0100] rev 59189
Isabelle2015 NEWS: "^^^" handles negative numerals differently
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 07 Dec 2015 14:10:59 +0100] rev 59188
Isabelle2014-->15: closed Thm.thy applied to tests
Note:
# concerns the funs: assbl_thm, cterm_of-->global_cterm_of, make_thm,
prop_of, rep_thm, rep_thm_G, therm_of.
# tests have not been run since start of Isabelle2014-->15.
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 07 Dec 2015 11:32:12 +0100] rev 59187
Isabelle2014-->15: rem_thm-->Thm.rep_thm
Note: Isabelle/Isac now compiles with the (probably last) error:
"~/proto4/libisabelle/libisabelle/src/main/isabelle/Protocol/Protocol"
Unfinished theory
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 07 Dec 2015 11:25:02 +0100] rev 59186
Isabelle2014-->15: term_of-->Thm.term_of
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 07 Dec 2015 10:52:07 +0100] rev 59185
Isabelle2014-->15: Thm.thy is not open anymore, further funs qualified
Notes:
# The funs are: Thm.assbl_thm, Thm.make_thm, Thm.rep_thm_G
# xmlsrc/thy-hierarchy.sml:make_thm now different
# Thm.term_of done in the next changeset.
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 07 Dec 2015 10:17:08 +0100] rev 59184
sabelle2014-->15: cterm_of-->Thm.global_cterm_of
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 07 Dec 2015 10:01:49 +0100] rev 59183
Isabelle2014-->15: prop_of-->Thm.prop_of
Walther Neuper <wneuper@ist.tugraz.at> [Mon, 07 Dec 2015 09:52:54 +0100] rev 59182
documented structure for inital imports
Notes: structure inherited from migration which began with Isabelle2009.
Not changed. Improve?
Walther Neuper <wneuper@ist.tugraz.at> [Sun, 06 Dec 2015 08:45:16 +0100] rev 59181
merged Isac's hooks into Isabelle
Walther Neuper <wneuper@ist.tugraz.at> [Sat, 05 Dec 2015 16:09:41 +0100] rev 59180
switched from Isabelle2014 to Isabelle2015, intermediate state
Note: we dropped jEditC, since libisabelle took over.