isabelle: File revisions

src/Pure/Isar/class_target.ML

2010-03-20	wenzelm	2010-03-20	renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;	file \| diff \| annotate
2010-03-09	wenzelm	2010-03-09	added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;	file \| diff \| annotate
2010-02-23	haftmann	2010-02-23	dropped axclass	file \| diff \| annotate
2010-02-15	haftmann	2010-02-15	clarifed type	file \| diff \| annotate
2010-02-07	wenzelm	2010-02-07	renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;	file \| diff \| annotate
2009-11-30	haftmann	2009-11-30	dropped some unused bindings	file \| diff \| annotate
2009-11-30	haftmann	2009-11-30	more accurate linerarity	file \| diff \| annotate
2009-11-13	wenzelm	2009-11-13	modernized structure Local_Theory;	file \| diff \| annotate
2009-11-08	wenzelm	2009-11-08	adapted Theory_Data; tuned;	file \| diff \| annotate
2009-11-08	wenzelm	2009-11-08	adapted Generic_Data, Proof_Data; tuned;	file \| diff \| annotate
2009-10-25	wenzelm	2009-10-25	eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;	file \| diff \| annotate
2009-10-17	wenzelm	2009-10-17	operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;	file \| diff \| annotate
2009-10-17	wenzelm	2009-10-17	indicate CRITICAL nature of various setmp combinators;	file \| diff \| annotate
2009-10-01	haftmann	2009-10-01	proper merge of interpretation equations	file \| diff \| annotate
2009-10-01	ballarin	2009-10-01	Merged.	file \| diff \| annotate
2009-08-19	ballarin	2009-08-19	Improved comments and api names.	file \| diff \| annotate
2009-08-15	haftmann	2009-08-15	additional checkpoints avoid problems in error situations	file \| diff \| annotate
2009-07-15	haftmann	2009-07-15	simplification of locale interfaces	file \| diff \| annotate
2009-07-10	haftmann	2009-07-10	tuned locale interface	file \| diff \| annotate
2009-06-29	haftmann	2009-06-29	mutual instances	file \| diff \| annotate
2009-06-17	haftmann	2009-06-17	stripped dead comment	file \| diff \| annotate
2009-06-14	haftmann	2009-06-14	axclass command now legacy	file \| diff \| annotate
2009-06-09	haftmann	2009-06-09	tuned make/map/merge combinators	file \| diff \| annotate
2009-05-24	haftmann	2009-05-24	tuned class user space type system code	file \| diff \| annotate
2009-05-20	haftmann	2009-05-20	tuned	file \| diff \| annotate
2009-05-20	haftmann	2009-05-20	avoid potential problem with stale theory	file \| diff \| annotate
2009-04-28	haftmann	2009-04-28	prevent potential failure	file \| diff \| annotate
2009-03-28	wenzelm	2009-03-28	simplified Locale.activate operations, using generic context; misc tuning;	file \| diff \| annotate
2009-03-13	wenzelm	2009-03-13	merged	file \| diff \| annotate
2009-03-13	haftmann	2009-03-13	coherent binding policy with primitive target operations	file \| diff \| annotate
2009-03-13	wenzelm	2009-03-13	simplified method setup;	file \| diff \| annotate
2009-03-13	wenzelm	2009-03-13	unified type Proof.method and pervasive METHOD combinators;	file \| diff \| annotate
2009-03-08	wenzelm	2009-03-08	moved basic algebra of long names from structure NameSpace to Long_Name;	file \| diff \| annotate
2009-03-07	wenzelm	2009-03-07	more uniform handling of binding in targets and derived elements;	file \| diff \| annotate
2009-03-05	wenzelm	2009-03-05	renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;	file \| diff \| annotate
2009-02-18	haftmann	2009-02-18	more precise improvement in instantiation user space type system	file \| diff \| annotate
2009-01-26	haftmann	2009-01-26	fixed reading of class specs: declare class operations in context	file \| diff \| annotate
2009-01-21	haftmann	2009-01-21	allow empty class specs	file \| diff \| annotate
2009-01-21	haftmann	2009-01-21	code cleanup	file \| diff \| annotate
2009-01-19	haftmann	2009-01-19	improved tackling of subclasses	file \| diff \| annotate
2009-01-17	haftmann	2009-01-17	tuned signature	file \| diff \| annotate
2009-01-17	haftmann	2009-01-17	code cleanup	file \| diff \| annotate
2009-01-16	haftmann	2009-01-16	migrated class package to new locale implementation	file \| diff \| annotate
2009-01-11	haftmann	2009-01-11	construct explicit class morphism	file \| diff \| annotate
2009-01-06	haftmann	2009-01-06	locale -> old_locale, new_locale -> locale	file \| diff \| annotate
2009-01-05	haftmann	2009-01-05	locale -> old_locale, new_locale -> locale	file \| diff \| annotate
2009-01-05	haftmann	2009-01-05	rearranged target theories	file \| diff \| annotate \| base

isabelle

RSS Atom