isabelle: File revisions

src/Pure/Syntax/syntax.ML

2007-11-10	wenzelm	2007-11-10	added update_const_gram (avoids duplicates); tuned;	file \| diff \| annotate
2007-10-20	wenzelm	2007-10-20	moved internalM to PrintMode.internal; PrintMode.input;	file \| diff \| annotate
2007-10-16	wenzelm	2007-10-16	Syntax.(un)check: explicit result option;	file \| diff \| annotate
2007-10-15	wenzelm	2007-10-15	unparse_arity: unparse type constructor as well;	file \| diff \| annotate
2007-10-11	wenzelm	2007-10-11	renamed Syntax.XXX_mode to Syntax.mode_XXX; moved ProofContext.pp to Syntax.pp;	file \| diff \| annotate
2007-10-09	wenzelm	2007-10-09	generic Syntax.pretty/string_of operations; added uncheck/unparse_classrel/arity (from sign.ML); tuned;	file \| diff \| annotate
2007-09-29	wenzelm	2007-09-29	added unparse interfaces (still unused); add_typ/term_check: added stage and name argument; added print_checks;	file \| diff \| annotate
2007-09-25	wenzelm	2007-09-25	removed redundant global_parse operations; renamed global_XXX to XXX_global;	file \| diff \| annotate
2007-09-23	wenzelm	2007-09-23	TypeInfer.constrain: canonical argument order;	file \| diff \| annotate
2007-09-17	wenzelm	2007-09-17	added print_mode_value (CRITICAL);	file \| diff \| annotate
2007-09-01	wenzelm	2007-09-01	added singleton check_typ/term/prop;	file \| diff \| annotate
2007-08-30	wenzelm	2007-08-30	turned type_check into separate typ/term_check; tuned sifnature;	file \| diff \| annotate
2007-08-20	wenzelm	2007-08-20	standard_parse_term: added pp/check argument, include disambig here (from sign.ML);	file \| diff \| annotate
2007-08-20	wenzelm	2007-08-20	type_check: tuned singleton funs case;	file \| diff \| annotate
2007-08-14	wenzelm	2007-08-14	renamed standard_read_XXX to standard_parse_XXX; added global_read/parse_XXX;	file \| diff \| annotate
2007-08-14	wenzelm	2007-08-14	added generic wrapper for parse/read functions; renamed read_term to standard_read_term etc.;	file \| diff \| annotate
2007-08-13	wenzelm	2007-08-13	moved appl syntax to PureThy; structure Lexicon: not hidden;	file \| diff \| annotate
2007-07-23	wenzelm	2007-07-23	hide internal structures (again);	file \| diff \| annotate
2007-07-09	wenzelm	2007-07-09	type output = string indicates raw system output;	file \| diff \| annotate
2007-07-08	wenzelm	2007-07-08	replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;	file \| diff \| annotate
2007-07-07	wenzelm	2007-07-07	pretty_sort/typ/term: markup;	file \| diff \| annotate
2007-07-07	wenzelm	2007-07-07	simplified pretty token metric: type int;	file \| diff \| annotate
2007-04-21	wenzelm	2007-04-21	TypeExt.decode_term;	file \| diff \| annotate
2007-04-15	wenzelm	2007-04-15	added read_term; adapted decoding of types/sorts;	file \| diff \| annotate
2007-04-03	wenzelm	2007-04-03	avoid clash with Alice keywords;	file \| diff \| annotate
2007-01-19	wenzelm	2007-01-19	tuned Scan.extend_lexicon;	file \| diff \| annotate
2006-12-30	wenzelm	2006-12-30	removed conditional combinator;	file \| diff \| annotate
2006-12-13	wenzelm	2006-12-13	tuned signature;	file \| diff \| annotate
2006-12-11	wenzelm	2006-12-11	advanced translation functions: Proof.context;	file \| diff \| annotate
2006-12-09	wenzelm	2006-12-09	added internal_mode;	file \| diff \| annotate
2006-12-07	wenzelm	2006-12-07	added input_mode;	file \| diff \| annotate
2006-11-26	wenzelm	2006-11-26	extend_trtab: allow identical trfuns to be overwritten;	file \| diff \| annotate
2006-09-29	wenzelm	2006-09-29	Syntax.mode;	file \| diff \| annotate
2006-09-21	wenzelm	2006-09-21	member (op =);	file \| diff \| annotate
2006-05-02	wenzelm	2006-05-02	extend/remove_syntax: observe inout flag for translations, too;	file \| diff \| annotate
2006-04-27	wenzelm	2006-04-27	tuned basic list operators (flat, maps, map_filter);	file \| diff \| annotate
2006-04-08	wenzelm	2006-04-08	pretty_term: late externing of consts (support authentic syntax);	file \| diff \| annotate
2006-03-21	wenzelm	2006-03-21	subtract (op =);	file \| diff \| annotate
2006-03-14	wenzelm	2006-03-14	added remove_trrules(_i); tuned;	file \| diff \| annotate
2006-02-15	wenzelm	2006-02-15	removed distinct, renamed gen_distinct to distinct;	file \| diff \| annotate
2006-02-08	haftmann	2006-02-08	introduced gen_distinct in place of distinct	file \| diff \| annotate
2006-02-07	wenzelm	2006-02-07	renamed gen_duplicates to duplicates;	file \| diff \| annotate
2006-02-06	wenzelm	2006-02-06	TableFun: renamed xxx_multi to xxx_list;	file \| diff \| annotate
2006-02-03	wenzelm	2006-02-03	canonical member/insert/merge;	file \| diff \| annotate
2006-01-31	wenzelm	2006-01-31	advanced translations: Context.generic;	file \| diff \| annotate
2006-01-19	wenzelm	2006-01-19	added basic syntax; removed pure syntax;	file \| diff \| annotate
2006-01-14	wenzelm	2006-01-14	sane ERROR handling;	file \| diff \| annotate
2005-12-17	wenzelm	2005-12-17	sort_distinct;	file \| diff \| annotate
2005-09-20	haftmann	2005-09-20	slight adaptions to library changes	file \| diff \| annotate
2005-09-15	wenzelm	2005-09-15	TableFun/Symtab: curried lookup and update;	file \| diff \| annotate
2005-09-08	haftmann	2005-09-08	introduces some modern-style AList operations	file \| diff \| annotate
2005-09-01	wenzelm	2005-09-01	curried_lookup/update;	file \| diff \| annotate
2005-08-31	wenzelm	2005-08-31	fixed ins_tokentr: AList.default;	file \| diff \| annotate
2005-08-31	haftmann	2005-08-31	introduced AList.*	file \| diff \| annotate
2005-08-28	wenzelm	2005-08-28	removed obsolete type_syn;	file \| diff \| annotate
2005-08-16	wenzelm	2005-08-16	added eq_syntax;	file \| diff \| annotate
2005-07-06	wenzelm	2005-07-06	tuned msg;	file \| diff \| annotate
2005-07-01	wenzelm	2005-07-01	ambig msg: warning again;	file \| diff \| annotate
2005-07-01	wenzelm	2005-07-01	use tracing for potentially voluminous ambiguity output;	file \| diff \| annotate
2005-06-29	wenzelm	2005-06-29	proper treatment of advanced trfuns: pass thy argument; tuned warning;	file \| diff \| annotate

isabelle

RSS Atom