#
ebbec143 |
|
17-Feb-2020 |
paulson <lp15@cam.ac.uk> |
a few new lemmas
|
#
927141b3 |
|
23-Oct-2019 |
haftmann <none@none> |
tuned syntax
|
#
caa31cef |
|
22-Jun-2019 |
haftmann <none@none> |
streamlined setup for linear algebra, particularly removed redundant rule declarations
|
#
a6af7849 |
|
14-May-2019 |
paulson <lp15@cam.ac.uk> |
Generalisations involving numerals; comparisons should now work for ennreal
|
#
fe03936a |
|
01-May-2019 |
haftmann <none@none> |
more lemmas --HG-- extra : rebase_source : 3e2ac977160873ea4b0f5fb90c505d1a2c674b91
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
14f1ca5d |
|
28-Jun-2018 |
wenzelm <none@none> |
avoid pending shyps in global theory facts;
|
#
0c0e3425 |
|
03-Apr-2018 |
haftmann <none@none> |
more rules for numeral conversions; more precise code setup for pred_numeral
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
f827427c |
|
02-Dec-2017 |
haftmann <none@none> |
cleaned up and tuned --HG-- extra : rebase_source : a1262817f08e7c73c1f578e8c3b21fcf9314f1fb
|
#
711c1878 |
|
30-Oct-2017 |
haftmann <none@none> |
tuned some proofs and added some lemmas --HG-- extra : rebase_source : ad93f195ceb7a124396a911453e61f00f52999be
|
#
869cd6da |
|
17-Jul-2017 |
eberlm <eberlm@in.tum.de> |
Printing natural numbers as numerals in evaluation --HG-- extra : amend_source : d893fca71b1eff819db8901dfa1a670f16a5dc0e
|
#
294b469b |
|
16-Oct-2016 |
haftmann <none@none> |
de-orphanized declaration
|
#
70525112 |
|
12-Oct-2016 |
haftmann <none@none> |
transfer lifting rule for numeral --HG-- extra : rebase_source : bafc2cb3fd6a49a365472e2fb15a4de692ec874d
|
#
ed540129 |
|
18-Sep-2016 |
Lars Hupel <lars.hupel@mytum.de> |
tuned
|
#
1667fe95 |
|
10-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
8175ce0f |
|
12-Mar-2016 |
haftmann <none@none> |
model characters directly as range 0..255 * * * operate on syntax terms rather than asts
|
#
70cb89b7 |
|
01-Mar-2016 |
haftmann <none@none> |
tuned bootstrap order to provide type classes in a more sensible order --HG-- extra : rebase_source : b4008b5f377525bc1866d515a16702fbb0b463c9
|
#
e3b38c13 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings
|
#
08cabf03 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "abs";
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
3487f527 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
#
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
34ef1352 |
|
10-Apr-2015 |
wenzelm <none@none> |
tuned signature;
|
#
ac517014 |
|
31-Mar-2015 |
haftmann <none@none> |
given up separate type classes demanding `inverse 0 = 0`
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
b7351c6c |
|
02-Oct-2014 |
haftmann <none@none> |
moved lemmas out of Int.thy which have nothing to do with int --HG-- extra : rebase_source : a6db16c774c1c078a2ed1a129509da61fa662a39
|
#
17db18c6 |
|
22-Sep-2014 |
wenzelm <none@none> |
discontinued old "xnum" token category; simplified Lexicon.read_num, Lexicon.read_float: no sign here; express ZF numerals via "num" with mixfix grammar; recovered printing of ZF numerals: "one" is abbreviation;
|
#
6a02610c |
|
21-Sep-2014 |
haftmann <none@none> |
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
|
#
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
#
ecb6646e |
|
02-Sep-2014 |
blanchet <none@none> |
tuned imports
|
#
1ba740de |
|
02-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' in 'Main'
|
#
2326a269 |
|
01-Sep-2014 |
blanchet <none@none> |
renamed BNF theories --HG-- rename : src/HOL/BNF_Comp.thy => src/HOL/BNF_Composition.thy rename : src/HOL/BNF_FP_Base.thy => src/HOL/BNF_Fixpoint_Base.thy rename : src/HOL/BNF_GFP.thy => src/HOL/BNF_Greatest_Fixpoint.thy rename : src/HOL/BNF_LFP.thy => src/HOL/BNF_Least_Fixpoint.thy
|
#
fb2f6a3a |
|
01-Sep-2014 |
blanchet <none@none> |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place --HG-- rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
acab6ad5 |
|
07-Mar-2014 |
wenzelm <none@none> |
more official const syntax: avoid educated guessing by Syntax_Phases.decode_term;
|
#
3154df20 |
|
17-Feb-2014 |
blanchet <none@none> |
renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
|
#
40e0ba91 |
|
12-Feb-2014 |
blanchet <none@none> |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
#
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
#
7ac6d7e8 |
|
04-Nov-2013 |
haftmann <none@none> |
streamlined setup of linear arithmetic
|
#
d2ef840a |
|
01-Nov-2013 |
haftmann <none@none> |
more simplification rules on unary and binary minus --HG-- extra : rebase_source : 7c88c9f33c4be8eae76f508a1a73ba79c8b769b1
|
#
9635d322 |
|
18-Aug-2013 |
haftmann <none@none> |
generalized sort constraint of lemmas
|
#
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier --HG-- extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
#
808c8efd |
|
28-May-2013 |
wenzelm <none@none> |
more explicit Printer.type_emphasis, depending on show_type_emphasis; tuned signature;
|
#
c414b995 |
|
27-May-2013 |
wenzelm <none@none> |
tuned;
|
#
ffcd6989 |
|
25-May-2013 |
wenzelm <none@none> |
syntax translations always depend on context;
|
#
5a8927d0 |
|
15-Feb-2013 |
haftmann <none@none> |
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 --HG-- extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17
|
#
de166af7 |
|
11-Jan-2013 |
haftmann <none@none> |
sharing of recursive results on evaluation
|
#
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
#
a8d61ae3 |
|
03-Oct-2012 |
wenzelm <none@none> |
more explicit show_type_constraint, show_sort_constraint;
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
1d753fd8 |
|
02-Apr-2012 |
huffman <none@none> |
remove unnecessary qualifiers on names
|
#
3ba04619 |
|
02-Apr-2012 |
huffman <none@none> |
add lemma Suc_1
|
#
2a20d32d |
|
01-Apr-2012 |
huffman <none@none> |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
#
09ca59ef |
|
30-Mar-2012 |
huffman <none@none> |
load Tools/numeral.ML in Num.thy
|
#
830bc8e7 |
|
30-Mar-2012 |
huffman <none@none> |
tuned proof
|
#
ff4bed69 |
|
30-Mar-2012 |
huffman <none@none> |
set up numeral reorient simproc in Num.thy
|
#
1d4dd90e |
|
29-Mar-2012 |
huffman <none@none> |
replace lemmas eval_nat_numeral with a simpler reformulation
|
#
b6f870f0 |
|
30-Mar-2012 |
huffman <none@none> |
new lemmas for simplifying subtraction on nat numerals
|
#
5ab3dd35 |
|
30-Mar-2012 |
huffman <none@none> |
move more theorems from Nat_Numeral.thy to Num.thy
|
#
edc4a0e7 |
|
30-Mar-2012 |
huffman <none@none> |
fix search-and-replace errors --HG-- extra : transplant_source : %23%E0%CF%2C%AB%B0%A9%F3%CF1%E2%04ophV%BA%7E7C
|
#
dffabb9f |
|
30-Mar-2012 |
huffman <none@none> |
add constant pred_numeral k = numeral k - (1::nat); replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral
|
#
0f623881 |
|
30-Mar-2012 |
huffman <none@none> |
move lemmas from Nat_Numeral to Int.thy and Num.thy
|
#
e7c93f0a |
|
29-Mar-2012 |
huffman <none@none> |
move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy
|
#
2fe41edf |
|
29-Mar-2012 |
huffman <none@none> |
bootstrap Num.thy before Power.thy; move lemmas about powers into Power.thy
|
#
6c4c92be |
|
26-Mar-2012 |
huffman <none@none> |
fix incorrect code_modulename declarations
|
#
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|