haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 52872
brittleness stamping for local theories
haftmann [Tue, 23 Apr 2013 11:14:50 +0200] rev 52871
tuned
immler [Mon, 22 Apr 2013 18:39:12 +0200] rev 52870
removed type constraints
hoelzl [Mon, 22 Apr 2013 16:36:02 +0200] rev 52869
NEWS
haftmann [Sun, 21 Apr 2013 20:08:13 +0200] rev 52868
more sharing
haftmann [Sun, 21 Apr 2013 16:29:40 +0200] rev 52867
interpretation: distinguish theories and proofs by explicit parameter rather than generic context;
formal initialisation of theory target during interpretation;
prefer Local_Theory.notes_kind to register mixin equations during interpretation;
more uniformity between note_eqns_register and note_eqns_dependency
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 52866
dropped unusued identifier
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 52865
avoid odd bifurcation with Attrib.local_notes vs. Locale.add_thmss -- n.b. note_eqns_dependency operates in a specific locale target
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 52864
tuned for uniformity
haftmann [Sun, 21 Apr 2013 10:41:18 +0200] rev 52863
reflection as official HOL tool