isabelle: File revisions

src/HOL/Library/old_recdef.ML

2015-12-09	wenzelm	2015-12-09	clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;	file \| diff \| annotate
2015-10-17	wenzelm	2015-10-17	tuned signature;	file \| diff \| annotate
2015-10-13	haftmann	2015-10-13	prod_case as canonical name for product type eliminator	file \| diff \| annotate
2015-09-25	wenzelm	2015-09-25	moved remaining display.ML to more_thm.ML;	file \| diff \| annotate
2015-09-06	haftmann	2015-09-06	prefer "uncurry" as canonical name for case distinction on products in combinatorial view	file \| diff \| annotate
2015-08-28	wenzelm	2015-08-28	tuned;	file \| diff \| annotate
2015-08-16	wenzelm	2015-08-16	added Thm.chyps_of; eliminated Thm.cprep_thm, with its potentially ill-typed (!) tpairs (cf. c9ad3e64ddcf);	file \| diff \| annotate
2015-07-28	wenzelm	2015-07-28	more explicit context; tuned signature;	file \| diff \| annotate
2015-07-25	wenzelm	2015-07-25	updated to infer_instantiate; tuned;	file \| diff \| annotate
2015-07-24	wenzelm	2015-07-24	proper context;	file \| diff \| annotate
2015-07-18	wenzelm	2015-07-18	prefer tactics with explicit context;	file \| diff \| annotate
2015-07-09	wenzelm	2015-07-09	clarified context; eliminated dead code;	file \| diff \| annotate
2015-07-05	wenzelm	2015-07-05	simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);	file \| diff \| annotate
2015-06-19	wenzelm	2015-06-19	removed dead code;	file \| diff \| annotate
2015-06-19	wenzelm	2015-06-19	discontinued unused 'defer_recdef';	file \| diff \| annotate
2015-06-19	wenzelm	2015-06-19	tuned;	file \| diff \| annotate
2015-06-19	wenzelm	2015-06-19	removed dead code;	file \| diff \| annotate
2015-06-19	wenzelm	2015-06-19	moved sources;	file \| diff \| annotate

isabelle

RSS Atom