isabelle: File revisions

src/HOL/Num.thy

2014-03-07	wenzelm	2014-03-07	more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;	file \| diff \| annotate
2014-02-17	blanchet	2014-02-17	renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)	file \| diff \| annotate
2014-02-12	blanchet	2014-02-12	renamed 'nat_{case,rec}' to '{case,rec}_nat'	file \| diff \| annotate
2013-11-19	haftmann	2013-11-19	eliminiated neg_numeral in favour of - (numeral _)	file \| diff \| annotate
2013-11-04	haftmann	2013-11-04	streamlined setup of linear arithmetic	file \| diff \| annotate
2013-11-01	haftmann	2013-11-01	more simplification rules on unary and binary minus	file \| diff \| annotate
2013-08-18	haftmann	2013-08-18	generalized sort constraint of lemmas	file \| diff \| annotate
2013-06-23	haftmann	2013-06-23	migration from code_(const\|type\|class\|instance) to code_printing and from code_module to code_identifier	file \| diff \| annotate
2013-05-28	wenzelm	2013-05-28	more explicit Printer.type_emphasis, depending on show_type_emphasis; tuned signature;	file \| diff \| annotate
2013-05-27	wenzelm	2013-05-27	tuned;	file \| diff \| annotate
2013-05-25	wenzelm	2013-05-25	syntax translations always depend on context;	file \| diff \| annotate
2013-02-15	haftmann	2013-02-15	two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one	file \| diff \| annotate
2013-01-11	haftmann	2013-01-11	sharing of recursive results on evaluation	file \| diff \| annotate
2012-10-19	webertj	2012-10-19	Renamed {left,right}_distrib to distrib_{right,left}.	file \| diff \| annotate
2012-10-03	wenzelm	2012-10-03	more explicit show_type_constraint, show_sort_constraint;	file \| diff \| annotate
2012-08-22	wenzelm	2012-08-22	prefer ML_file over old uses;	file \| diff \| annotate
2012-04-02	huffman	2012-04-02	remove unnecessary qualifiers on names	file \| diff \| annotate
2012-04-02	huffman	2012-04-02	add lemma Suc_1	file \| diff \| annotate
2012-04-01	huffman	2012-04-01	removed Nat_Numeral.thy, moving all theorems elsewhere	file \| diff \| annotate
2012-03-30	huffman	2012-03-30	load Tools/numeral.ML in Num.thy	file \| diff \| annotate
2012-03-30	huffman	2012-03-30	tuned proof	file \| diff \| annotate
2012-03-30	huffman	2012-03-30	set up numeral reorient simproc in Num.thy	file \| diff \| annotate
2012-03-30	huffman	2012-03-30	replace lemmas eval_nat_numeral with a simpler reformulation	file \| diff \| annotate
2012-03-30	huffman	2012-03-30	new lemmas for simplifying subtraction on nat numerals	file \| diff \| annotate
2012-03-30	huffman	2012-03-30	move more theorems from Nat_Numeral.thy to Num.thy	file \| diff \| annotate
2012-03-30	huffman	2012-03-30	fix search-and-replace errors	file \| diff \| annotate
2012-03-30	huffman	2012-03-30	add constant pred_numeral k = numeral k - (1::nat); replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral	file \| diff \| annotate
2012-03-30	huffman	2012-03-30	move lemmas from Nat_Numeral to Int.thy and Num.thy	file \| diff \| annotate
2012-03-29	huffman	2012-03-29	move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy	file \| diff \| annotate
2012-03-29	huffman	2012-03-29	bootstrap Num.thy before Power.thy; move lemmas about powers into Power.thy	file \| diff \| annotate
2012-03-26	huffman	2012-03-26	fix incorrect code_modulename declarations	file \| diff \| annotate
2012-03-25	huffman	2012-03-25	merged fork with new numeral representation (see NEWS)	file \| diff \| annotate

isabelle

RSS Atom