| #
53513bfd |
|
24-May-2018 |
haftmann <none@none> |
treat gcd_eq_1_imp_coprime analogously to mod_0_imp_dvd
--HG--
extra : rebase_source : 634f08eaeef46ac7c528067d98f136d5bbd3ce01
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
3e62aabe |
|
02-Dec-2017 |
haftmann <none@none> |
more simplification rules
--HG--
extra : rebase_source : 2b7704ac9459d132ec9fea4769b865bdcad1548f
|
| #
85b3e948 |
|
11-Nov-2017 |
haftmann <none@none> |
dedicated definition for coprimality
--HG--
extra : rebase_source : 891168c98ce62efae6b7e72c7d3365fea12b33ae
|
| #
711c1878 |
|
30-Oct-2017 |
haftmann <none@none> |
tuned some proofs and added some lemmas
--HG--
extra : rebase_source : ad93f195ceb7a124396a911453e61f00f52999be
|
| #
eda74618 |
|
09-Oct-2017 |
haftmann <none@none> |
tuned imports
--HG--
extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011
|
| #
f740f805 |
|
08-Oct-2017 |
haftmann <none@none> |
more fundamental definition of div and mod on int
--HG--
extra : rebase_source : 95b72d036b88e199c61235ea5833a905f5632800
|
| #
f601f95d |
|
08-Oct-2017 |
haftmann <none@none> |
avoid trivial definition
--HG--
extra : rebase_source : ecbfc9db3f916d9cc1908f888bce3612ed449b8c
|
| #
7694f309 |
|
08-Oct-2017 |
haftmann <none@none> |
tuned proofs
--HG--
extra : rebase_source : c340467182f151fe79f1b5f75f2c46bf5bbf636e
|
| #
3a436e5d |
|
11-May-2017 |
haftmann <none@none> |
more lemmas
--HG--
extra : rebase_source : e39561a47214aaf67eea524bde7eb12dcffc8801
|
| #
5f50f074 |
|
23-Apr-2017 |
haftmann <none@none> |
include GCD as integral part of computational algebra in session HOL
|
| #
3f30d088 |
|
22-Apr-2017 |
wenzelm <none@none> |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
--HG--
rename : src/HOL/Main.thy => src/HOL/Pre_Main.thy
|
| #
688d9965 |
|
09-Jan-2017 |
haftmann <none@none> |
gcd/lcm on finite sets
--HG--
extra : rebase_source : 0af6f75cb4b38f565ff2fa19edffbb8abf6de500
|
| #
8863117a |
|
17-Dec-2016 |
haftmann <none@none> |
restructured matter on polynomials and normalized fractions
--HG--
extra : rebase_source : 71508900ff150d54097ae5c4c2da7176f09cb625
|
| #
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
| #
54a0a039 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized theorem names for facts involving the div and mod identity
|
| #
7cb68da2 |
|
16-Oct-2016 |
haftmann <none@none> |
more standardized names
|
| #
23930628 |
|
18-Sep-2016 |
haftmann <none@none> |
more generic algebraic lemmas
--HG--
extra : rebase_source : afd1b38644ce9418dc6eeaf977c35a8502e396b5
|
| #
6d0b05b4 |
|
18-Sep-2016 |
wenzelm <none@none> |
tuned proofs;
|
| #
131dfaff |
|
15-Sep-2016 |
nipkow <none@none> |
renamed listsum -> sum_list, listprod ~> prod_list
|
| #
7655367b |
|
14-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
| #
ae5f3742 |
|
01-Jul-2016 |
Manuel Eberl <eberlm@in.tum.de> |
More lemmas on Gcd/Lcm
|
| #
ddacf0c0 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
606057a5 |
|
18-Apr-2016 |
haftmann <none@none> |
capitalized GCD and LCM syntax
--HG--
extra : rebase_source : d31f2569a9c4fe6840d8020d84630dfd542c38aa
|
| #
0a4555c1 |
|
26-Feb-2016 |
Manuel Eberl <eberlm@in.tum.de> |
Tuned Euclidean Rings/GCD rings
|
| #
069896e9 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings and tuned proofs
|
| #
15ef9377 |
|
17-Feb-2016 |
haftmann <none@none> |
more sophisticated GCD syntax
|
| #
b376ab94 |
|
17-Feb-2016 |
haftmann <none@none> |
cleansed junk-producing interpretations for gcd/lcm on nat altogether
|
| #
e3b38c13 |
|
17-Feb-2016 |
haftmann <none@none> |
dropped various legacy fact bindings
|
| #
a6f23363 |
|
17-Feb-2016 |
haftmann <none@none> |
generalized some lemmas;
moved some lemmas in more appropriate places;
deleted potentially dangerous simp rule
|
| #
dec3b2c1 |
|
17-Feb-2016 |
haftmann <none@none> |
more theorems concerning gcd/lcm/Gcd/Lcm
|
| #
3765c1e0 |
|
17-Feb-2016 |
haftmann <none@none> |
further generalization and polishing
|
| #
9b9ee20c |
|
17-Feb-2016 |
haftmann <none@none> |
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
|
| #
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
| #
330d5073 |
|
30-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
d42838c4 |
|
28-Dec-2015 |
wenzelm <none@none> |
more symbols;
|
| #
08cabf03 |
|
27-Dec-2015 |
wenzelm <none@none> |
prefer symbols for "abs";
|
| #
5b82e735 |
|
24-Dec-2015 |
haftmann <none@none> |
tuned proofs and augmented lemmas
--HG--
extra : rebase_source : a111edd67831d78eb9b51d0bae9bb352ac5ffd0d
|
| #
4283eaa2 |
|
22-Dec-2015 |
haftmann <none@none> |
tuned proofs and augmented some lemmas
--HG--
extra : rebase_source : 87be06ebdfb36e627a8d034acf6a8e089cb44097
|
| #
3e03beca |
|
18-Dec-2015 |
Andreas Lochbihler <none@none> |
add gcd instance for integer and serialisation to target language operations
|
| #
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
420aaf4c |
|
12-Nov-2015 |
paulson <lp15@cam.ac.uk> |
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
|
| #
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
| #
8e8b881c |
|
04-Nov-2015 |
ballarin <none@none> |
Keyword 'rewrites' identifies rewrite morphisms.
|
| #
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
| #
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
| #
8ddc1a1c |
|
08-Jul-2015 |
haftmann <none@none> |
tuned facts
|
| #
b460013c |
|
08-Jul-2015 |
haftmann <none@none> |
more cautious use of [iff] declarations
|
| #
81da5767 |
|
08-Jul-2015 |
haftmann <none@none> |
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
|
| #
37b6e08d |
|
08-Jul-2015 |
haftmann <none@none> |
eliminated some duplication
|
| #
bddb8234 |
|
08-Jul-2015 |
haftmann <none@none> |
more algebraic properties for gcd/lcm
|
| #
9af6766f |
|
27-Jun-2015 |
haftmann <none@none> |
tuned code setup
|
| #
148b08d2 |
|
27-Jun-2015 |
haftmann <none@none> |
algebraic specification for set gcd
|
| #
5b7d639c |
|
25-Jun-2015 |
wenzelm <none@none> |
tuned proofs;
|
| #
da435e12 |
|
17-Jun-2015 |
wenzelm <none@none> |
tuned proofs -- slightly faster;
|
| #
b1f9bfee |
|
02-Jun-2015 |
wenzelm <none@none> |
tuned proof;
|
| #
d20797ec |
|
30-Apr-2015 |
paulson <lp15@cam.ac.uk> |
tidying some messy proofs
|
| #
b432d50c |
|
08-Apr-2015 |
wenzelm <none@none> |
eliminated hard tabs;
|
| #
f67d856d |
|
25-Mar-2015 |
wenzelm <none@none> |
prefer local fixes;
|
| #
08ee2a04 |
|
10-Mar-2015 |
paulson <lp15@cam.ac.uk> |
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
|
| #
40037c93 |
|
15-Feb-2015 |
haftmann <none@none> |
explicit equivalence for strict order on lattices
|
| #
ecb7ffea |
|
10-Feb-2015 |
wenzelm <none@none> |
indicate slow proof (approx. 20s);
|
| #
d2e2d432 |
|
17-Nov-2014 |
haftmann <none@none> |
formally self-contained gcd type classes
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
dc5a029e |
|
30-Oct-2014 |
haftmann <none@none> |
more simp rules concerning dvd and even/odd
--HG--
extra : rebase_source : 895ed3f871c22790e8d199a30828e91bc13bd735
|
| #
338f82d5 |
|
26-Oct-2014 |
haftmann <none@none> |
eliminated redundancies;
more simp rules
--HG--
extra : rebase_source : d2f3410108e72d87e8aafe6b8721e88136c940cf
|
| #
2227b563 |
|
24-Oct-2014 |
hoelzl <none@none> |
use NO_MATCH-simproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be non-terminating
|
| #
06e59c9f |
|
23-Oct-2014 |
haftmann <none@none> |
downshift of theory Parity in the hierarchy
|
| #
4a9ed335 |
|
07-Oct-2014 |
wenzelm <none@none> |
more bibtex entries;
more antiquotations;
|
| #
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
| #
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
| #
12157cd1 |
|
19-Mar-2014 |
haftmann <none@none> |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
| #
4f5ebd94 |
|
16-Mar-2014 |
haftmann <none@none> |
normalising simp rules for compound operators
|
| #
355cccc4 |
|
26-Dec-2013 |
haftmann <none@none> |
prefer ephemeral interpretation over interpretation in proof contexts;
prefer context begin ... end blocks for often-occuring assumptions;
slightly more complete interpretations into abstract algebraic structures for gcd/lcm
|
| #
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
| #
a61e722d |
|
15-Nov-2013 |
haftmann <none@none> |
proper code equations for Gcd and Lcm on nat and int
--HG--
extra : rebase_source : 455f8883402a3d1011b6105fe5b4e210549499c6
|
| #
d8c6c2fb |
|
05-Nov-2013 |
hoelzl <none@none> |
generalize SUP and INF to the syntactic type classes Sup and Inf
|
| #
1612e9ff |
|
25-Jul-2013 |
haftmann <none@none> |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
| #
192ca61e |
|
19-Jun-2013 |
noschinl <none@none> |
added coprimality lemma
|
| #
1dd2fd4a |
|
26-Mar-2013 |
haftmann <none@none> |
avoid odd foundational terms after interpretation;
more uniform code setup
--HG--
extra : rebase_source : 58e396fd054687bb2405f023bb6b8745872d2e64
|
| #
d4cae3bf |
|
23-Mar-2013 |
haftmann <none@none> |
fundamental revision of big operators on sets
|
| #
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
| #
c5a4229e |
|
27-Jul-2012 |
wenzelm <none@none> |
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
|
| #
764ae6e0 |
|
27-Dec-2011 |
haftmann <none@none> |
prefer canonical fold on lists
|
| #
64e2fca3 |
|
26-Oct-2011 |
huffman <none@none> |
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
|
| #
befc4880 |
|
24-Oct-2011 |
huffman <none@none> |
merge Gcd/GCD and Lcm/LCM
|
| #
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
| #
1947c572 |
|
08-Sep-2011 |
krauss <none@none> |
added syntactic classes for "inf" and "sup"
|
| #
363c25c4 |
|
07-Sep-2011 |
huffman <none@none> |
avoid using legacy theorem names
|
| #
29d7c97c |
|
06-Sep-2011 |
huffman <none@none> |
avoid using legacy theorem names
|
| #
7994d347 |
|
18-Aug-2011 |
haftmann <none@none> |
observe distinction between sets and predicates more properly
|
| #
180c955e |
|
20-May-2011 |
haftmann <none@none> |
names of fold_set locales resemble name of characteristic property more closely
|
| #
47bb2a89 |
|
21-Feb-2011 |
blanchet <none@none> |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
| #
6fb8be2b |
|
14-Jan-2011 |
wenzelm <none@none> |
eliminated global prems;
tuned proofs;
|
| #
5e72e9aa |
|
12-Jul-2010 |
haftmann <none@none> |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
| #
d1f69b8f |
|
26-Apr-2010 |
haftmann <none@none> |
dropped group_simps, ring_simps, field_eq_simps
|
| #
6fe63862 |
|
11-Mar-2010 |
haftmann <none@none> |
tuned prefixes of ac interpretations
|
| #
297293d7 |
|
08-Mar-2010 |
haftmann <none@none> |
transfer: avoid camel case
|
| #
485581a1 |
|
24-Feb-2010 |
haftmann <none@none> |
crossproduct coprimality lemmas
|
| #
aaaa7964 |
|
18-Feb-2010 |
huffman <none@none> |
get rid of many duplicate simp rule warnings
|
| #
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
| #
761011a7 |
|
28-Jan-2010 |
haftmann <none@none> |
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
|
| #
f94fe110 |
|
10-Jan-2010 |
berghofe <none@none> |
Adapted to changes in induct method.
|
| #
91dc9df8 |
|
01-Jan-2010 |
nipkow <none@none> |
added lemmas
|
| #
a815e441 |
|
01-Jan-2010 |
nipkow <none@none> |
added lemma
|
| #
a3119e9b |
|
01-Jan-2010 |
nipkow <none@none> |
removed FIXME
|
| #
d915d758 |
|
08-Dec-2009 |
haftmann <none@none> |
resorted code equations from "old" number theory version
|
| #
78944581 |
|
04-Dec-2009 |
nipkow <none@none> |
removed redundant lemma
|
| #
bacdb650 |
|
13-Nov-2009 |
nipkow <none@none> |
renamed lemmas "anti_sym" -> "antisym"
|
| #
7d4dc9b8 |
|
29-Oct-2009 |
haftmann <none@none> |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
| #
542f2bd2 |
|
23-Oct-2009 |
blanchet <none@none> |
continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
d0ba0630 |
|
06-Oct-2009 |
haftmann <none@none> |
added syntactic Inf and Sup
|
| #
700fe21b |
|
01-Sep-2009 |
haftmann <none@none> |
some reorganization of number theory
--HG--
rename : src/HOL/NewNumberTheory/Binomial.thy => src/HOL/Number_Theory/Binomial.thy
rename : src/HOL/NewNumberTheory/Cong.thy => src/HOL/Number_Theory/Cong.thy
rename : src/HOL/NewNumberTheory/Fib.thy => src/HOL/Number_Theory/Fib.thy
rename : src/HOL/NewNumberTheory/MiscAlgebra.thy => src/HOL/Number_Theory/MiscAlgebra.thy
rename : src/HOL/GCD.thy => src/HOL/Number_Theory/Primes.thy
rename : src/HOL/NewNumberTheory/ROOT.ML => src/HOL/Number_Theory/ROOT.ML
rename : src/HOL/NewNumberTheory/Residues.thy => src/HOL/Number_Theory/Residues.thy
rename : src/HOL/NewNumberTheory/UniqueFactorization.thy => src/HOL/Number_Theory/UniqueFactorization.thy
rename : src/HOL/NumberTheory/BijectionRel.thy => src/HOL/Old_Number_Theory/BijectionRel.thy
rename : src/HOL/NumberTheory/Chinese.thy => src/HOL/Old_Number_Theory/Chinese.thy
rename : src/HOL/NumberTheory/Euler.thy => src/HOL/Old_Number_Theory/Euler.thy
rename : src/HOL/NumberTheory/EulerFermat.thy => src/HOL/Old_Number_Theory/EulerFermat.thy
rename : src/HOL/NumberTheory/EvenOdd.thy => src/HOL/Old_Number_Theory/EvenOdd.thy
rename : src/HOL/NumberTheory/Factorization.thy => src/HOL/Old_Number_Theory/Factorization.thy
rename : src/HOL/NumberTheory/Fib.thy => src/HOL/Old_Number_Theory/Fib.thy
rename : src/HOL/NumberTheory/Finite2.thy => src/HOL/Old_Number_Theory/Finite2.thy
rename : src/HOL/NumberTheory/Gauss.thy => src/HOL/Old_Number_Theory/Gauss.thy
rename : src/HOL/NumberTheory/Int2.thy => src/HOL/Old_Number_Theory/Int2.thy
rename : src/HOL/NumberTheory/IntFact.thy => src/HOL/Old_Number_Theory/IntFact.thy
rename : src/HOL/NumberTheory/IntPrimes.thy => src/HOL/Old_Number_Theory/IntPrimes.thy
rename : src/HOL/Library/Legacy_GCD.thy => src/HOL/Old_Number_Theory/Legacy_GCD.thy
rename : src/HOL/Library/Pocklington.thy => src/HOL/Old_Number_Theory/Pocklington.thy
rename : src/HOL/Library/Primes.thy => src/HOL/Old_Number_Theory/Primes.thy
rename : src/HOL/NumberTheory/Quadratic_Reciprocity.thy => src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
rename : src/HOL/NumberTheory/ROOT.ML => src/HOL/Old_Number_Theory/ROOT.ML
rename : src/HOL/NumberTheory/Residues.thy => src/HOL/Old_Number_Theory/Residues.thy
rename : src/HOL/NumberTheory/WilsonBij.thy => src/HOL/Old_Number_Theory/WilsonBij.thy
rename : src/HOL/NumberTheory/WilsonRuss.thy => src/HOL/Old_Number_Theory/WilsonRuss.thy
rename : src/HOL/NumberTheory/document/root.tex => src/HOL/Old_Number_Theory/document/root.tex
|
| #
d018e244 |
|
26-Aug-2009 |
nipkow <none@none> |
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
|
| #
7f2e6294 |
|
21-Jul-2009 |
nipkow <none@none> |
Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM
|
| #
fd4d2448 |
|
21-Jul-2009 |
nipkow <none@none> |
Tests for executability of "prime"
|
| #
67d0648f |
|
15-Jul-2009 |
nipkow <none@none> |
Made "prime" executable
|
| #
265163d6 |
|
13-Jul-2009 |
berghofe <none@none> |
Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.
|
| #
79b2577f |
|
12-Jul-2009 |
nipkow <none@none> |
more gcd/lcm lemmas
|
| #
cc85a61a |
|
12-Jul-2009 |
nipkow <none@none> |
More about gcd/lcm, and some cleaning up
|
| #
7ec8d97b |
|
10-Jul-2009 |
avigad <none@none> |
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
|
| #
b274c339 |
|
07-Jul-2009 |
nipkow <none@none> |
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
|
| #
ed33049f |
|
26-Jun-2009 |
nipkow <none@none> |
lcm abs lemmas
|
| #
dfa2a0e4 |
|
26-Jun-2009 |
nipkow <none@none> |
gcd abs lemmas
|
| #
22184aea |
|
22-Jun-2009 |
nipkow <none@none> |
new lemmas
|
| #
525765f5 |
|
21-Jun-2009 |
nipkow <none@none> |
new lemmas
|
| #
6de99f81 |
|
20-Jun-2009 |
nipkow <none@none> |
added lemmas; tuned
|
| #
2e7487a3 |
|
19-Jun-2009 |
nipkow <none@none> |
new lemmas and tuning
|
| #
49c75aa4 |
|
18-Jun-2009 |
huffman <none@none> |
more [code del] declarations
|
| #
92773ae1 |
|
17-Jun-2009 |
huffman <none@none> |
new GCD library, courtesy of Jeremy Avigad
--HG--
rename : src/HOL/GCD.thy => src/HOL/Library/Legacy_GCD.thy
|
| #
ee8acb9f |
|
24-Jun-2009 |
nipkow <none@none> |
Cleaned up GCD
|
| #
262e6aa4 |
|
27-Mar-2009 |
haftmann <none@none> |
normalized imports
|
| #
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
| #
8f335aa9 |
|
24-Feb-2009 |
huffman <none@none> |
make more proofs work whether or not One_nat_def is a simp rule
|
| #
f9a8d2e1 |
|
21-Feb-2009 |
nipkow <none@none> |
Removed subsumed lemmas
|
| #
a7fd9c34 |
|
31-Jan-2009 |
nipkow <none@none> |
added some simp rules
|
| #
2f8489b9 |
|
28-Jan-2009 |
haftmann <none@none> |
Plain, Main form meeting points in import hierarchy
|
| #
f21befe1 |
|
03-Dec-2008 |
haftmann <none@none> |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
--HG--
rename : src/HOL/Library/Code_Message.thy => src/HOL/Code_Message.thy
rename : src/HOL/Complex/Complex.thy => src/HOL/Complex.thy
rename : src/HOL/Complex/Complex_Main.thy => src/HOL/Complex_Main.thy
rename : src/HOL/Real/ContNotDenum.thy => src/HOL/ContNotDenum.thy
rename : src/HOL/Hyperreal/Deriv.thy => src/HOL/Deriv.thy
rename : src/HOL/Hyperreal/Fact.thy => src/HOL/Fact.thy
rename : src/HOL/Hyperreal/FrechetDeriv.thy => src/HOL/FrechetDeriv.thy
rename : src/HOL/Library/GCD.thy => src/HOL/GCD.thy
rename : src/HOL/Hyperreal/Integration.thy => src/HOL/Integration.thy
rename : src/HOL/Real/Float.thy => src/HOL/Library/Float.thy
rename : src/HOL/Hyperreal/Lim.thy => src/HOL/Lim.thy
rename : src/HOL/Hyperreal/Ln.thy => src/HOL/Ln.thy
rename : src/HOL/Hyperreal/Log.thy => src/HOL/Log.thy
rename : src/HOL/Real/Lubs.thy => src/HOL/Lubs.thy
rename : src/HOL/Hyperreal/MacLaurin.thy => src/HOL/MacLaurin.thy
rename : src/HOL/Hyperreal/NthRoot.thy => src/HOL/NthRoot.thy
rename : src/HOL/Library/Order_Relation.thy => src/HOL/Order_Relation.thy
rename : src/HOL/Real/PReal.thy => src/HOL/PReal.thy
rename : src/HOL/Library/Parity.thy => src/HOL/Parity.thy
rename : src/HOL/Real/RComplete.thy => src/HOL/RComplete.thy
rename : src/HOL/Real/Rational.thy => src/HOL/Rational.thy
rename : src/HOL/Real/Real.thy => src/HOL/Real.thy
rename : src/HOL/Real/RealDef.thy => src/HOL/RealDef.thy
rename : src/HOL/Real/RealPow.thy => src/HOL/RealPow.thy
rename : src/HOL/Hyperreal/Series.thy => src/HOL/Series.thy
rename : src/HOL/Hyperreal/Taylor.thy => src/HOL/Taylor.thy
rename : src/HOL/arith_data.ML => src/HOL/Tools/arith_data.ML
rename : src/HOL/Real/float_arith.ML => src/HOL/Tools/float_arith.ML
rename : src/HOL/Real/float_syntax.ML => src/HOL/Tools/float_syntax.ML
rename : src/HOL/hologic.ML => src/HOL/Tools/hologic.ML
rename : src/HOL/int_arith1.ML => src/HOL/Tools/int_arith.ML
rename : src/HOL/int_factor_simprocs.ML => src/HOL/Tools/int_factor_simprocs.ML
rename : src/HOL/nat_simprocs.ML => src/HOL/Tools/nat_simprocs.ML
rename : src/HOL/Real/rat_arith.ML => src/HOL/Tools/rat_arith.ML
rename : src/HOL/Real/real_arith.ML => src/HOL/Tools/real_arith.ML
rename : src/HOL/simpdata.ML => src/HOL/Tools/simpdata.ML
rename : src/HOL/Hyperreal/Transcendental.thy => src/HOL/Transcendental.thy
rename : src/HOL/Library/RType.thy => src/HOL/Typerep.thy
rename : src/HOL/Library/Univ_Poly.thy => src/HOL/Univ_Poly.thy
rename : src/HOL/Complex/ex/Arithmetic_Series_Complex.thy => src/HOL/ex/Arithmetic_Series_Complex.thy
rename : src/HOL/Complex/ex/BigO_Complex.thy => src/HOL/ex/BigO_Complex.thy
rename : src/HOL/Complex/ex/HarmonicSeries.thy => src/HOL/ex/HarmonicSeries.thy
rename : src/HOL/Complex/ex/MIR.thy => src/HOL/ex/MIR.thy
rename : src/HOL/Complex/ex/ReflectedFerrack.thy => src/HOL/ex/ReflectedFerrack.thy
rename : src/HOL/Complex/ex/Sqrt.thy => src/HOL/ex/Sqrt.thy
rename : src/HOL/Complex/ex/Sqrt_Script.thy => src/HOL/ex/Sqrt_Script.thy
rename : src/HOL/Complex/ex/linrtac.ML => src/HOL/ex/linrtac.ML
rename : src/HOL/Complex/ex/mirtac.ML => src/HOL/ex/mirtac.ML
rename : src/Pure/Tools/quickcheck.ML => src/Tools/quickcheck.ML
rename : src/Pure/Tools/value.ML => src/Tools/value.ML
|
| #
285ae6c9 |
|
08-Jul-2005 |
nipkow <none@none> |
Used to be in Library/Primes
|