Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -10000 -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fri, 01 Jun 2007 10:44:31 +0200 rudimenary
changeset
haftmann [Fri, 01 Jun 2007 10:44:31 +0200] rev 23184
rudimenary
Fri, 01 Jun 2007 10:44:30 +0200 tuned
changeset
haftmann [Fri, 01 Jun 2007 10:44:30 +0200] rev 23183
tuned
Fri, 01 Jun 2007 10:44:28 +0200 dropped superfluous name bindings
changeset
haftmann [Fri, 01 Jun 2007 10:44:28 +0200] rev 23182
dropped superfluous name bindings
Fri, 01 Jun 2007 10:44:26 +0200 localized
changeset
haftmann [Fri, 01 Jun 2007 10:44:26 +0200] rev 23181
localized
Fri, 01 Jun 2007 10:44:24 +0200 fixed typo
changeset
haftmann [Fri, 01 Jun 2007 10:44:24 +0200] rev 23180
fixed typo
Thu, 31 May 2007 23:47:38 +0200 insert: canonical argument order;
changeset
wenzelm [Thu, 31 May 2007 23:47:38 +0200] rev 23179
insert: canonical argument order;
Thu, 31 May 2007 23:47:36 +0200 simplified/unified list fold;
changeset
wenzelm [Thu, 31 May 2007 23:47:36 +0200] rev 23178
simplified/unified list fold;
Thu, 31 May 2007 23:02:16 +0200 replace (- 1) with -1
changeset
huffman [Thu, 31 May 2007 23:02:16 +0200] rev 23177
replace (- 1) with -1
Thu, 31 May 2007 22:23:50 +0200 simplify some proofs
changeset
huffman [Thu, 31 May 2007 22:23:50 +0200] rev 23176
simplify some proofs
Thu, 31 May 2007 21:09:14 +0200 tuned headers -- adapted to usual conventions;
changeset
wenzelm [Thu, 31 May 2007 21:09:14 +0200] rev 23175
tuned headers -- adapted to usual conventions;
Thu, 31 May 2007 20:55:33 +0200 moved Compute_Oracle from Pure/Tools to Tools;
changeset
wenzelm [Thu, 31 May 2007 20:55:33 +0200] rev 23174
moved Compute_Oracle from Pure/Tools to Tools;
Thu, 31 May 2007 20:55:32 +0200 proper theory setup for compute oracle (based on CPure);
changeset
wenzelm [Thu, 31 May 2007 20:55:32 +0200] rev 23173
proper theory setup for compute oracle (based on CPure); simplified oracle setup;
Thu, 31 May 2007 20:55:31 +0200 moved IsaPlanner from Provers to Tools;
changeset
wenzelm [Thu, 31 May 2007 20:55:31 +0200] rev 23172
moved IsaPlanner from Provers to Tools; moved Compute_Oracle from Pure/Tools to Tools;
Thu, 31 May 2007 20:55:29 +0200 moved IsaPlanner from Provers to Tools;
changeset
wenzelm [Thu, 31 May 2007 20:55:29 +0200] rev 23171
moved IsaPlanner from Provers to Tools;
Thu, 31 May 2007 19:11:19 +0200 made aconvc pervasive;
changeset
wenzelm [Thu, 31 May 2007 19:11:19 +0200] rev 23170
made aconvc pervasive;
Thu, 31 May 2007 18:31:36 +0200 moved aconvc to more_thm.ML;
changeset
wenzelm [Thu, 31 May 2007 18:31:36 +0200] rev 23169
moved aconvc to more_thm.ML;
Thu, 31 May 2007 18:16:59 +0200 tuned ML setup;
changeset
wenzelm [Thu, 31 May 2007 18:16:59 +0200] rev 23168
tuned ML setup;
Thu, 31 May 2007 18:16:58 +0200 decode_term: force qualified name into Const;
changeset
wenzelm [Thu, 31 May 2007 18:16:58 +0200] rev 23167
decode_term: force qualified name into Const;
Thu, 31 May 2007 18:16:57 +0200 proper loading of ML files (in HOL.thy);
changeset
wenzelm [Thu, 31 May 2007 18:16:57 +0200] rev 23166
proper loading of ML files (in HOL.thy); moved Integ files to canonical place; misc cleanup;
Thu, 31 May 2007 18:16:54 +0200 HOL_proofs;
changeset
wenzelm [Thu, 31 May 2007 18:16:54 +0200] rev 23165
HOL_proofs;
Thu, 31 May 2007 18:16:52 +0200 moved Integ files to canonical place;
changeset
wenzelm [Thu, 31 May 2007 18:16:52 +0200] rev 23164
moved Integ files to canonical place;
Thu, 31 May 2007 18:16:51 +0200 proper loading of ML files;
changeset
wenzelm [Thu, 31 May 2007 18:16:51 +0200] rev 23163
proper loading of ML files;
Thu, 31 May 2007 18:16:50 +0200 removed dead code;
changeset
wenzelm [Thu, 31 May 2007 18:16:50 +0200] rev 23162
removed dead code;
Thu, 31 May 2007 18:16:47 +0200 tuned header;
changeset
wenzelm [Thu, 31 May 2007 18:16:47 +0200] rev 23161
tuned header;
Thu, 31 May 2007 18:16:46 +0200 doc: exclude isabelle_isar.pdf;
changeset
wenzelm [Thu, 31 May 2007 18:16:46 +0200] rev 23160
doc: exclude isabelle_isar.pdf;
Thu, 31 May 2007 15:23:35 +0200 tuned the proof
changeset
urbanc [Thu, 31 May 2007 15:23:35 +0200] rev 23159
tuned the proof
Thu, 31 May 2007 14:47:20 +0200 introduced symmetric variants of the lemmas for alpha-equivalence
changeset
urbanc [Thu, 31 May 2007 14:47:20 +0200] rev 23158
introduced symmetric variants of the lemmas for alpha-equivalence
Thu, 31 May 2007 14:34:09 +0200 proper loading of ML files;
changeset
wenzelm [Thu, 31 May 2007 14:34:09 +0200] rev 23157
proper loading of ML files; removed obsolete IFOL.thy/FOL.thy values;
Thu, 31 May 2007 14:34:07 +0200 removed obsolete IFOL.thy/FOL.thy values;
changeset
wenzelm [Thu, 31 May 2007 14:34:07 +0200] rev 23156
removed obsolete IFOL.thy/FOL.thy values;
Thu, 31 May 2007 14:34:06 +0200 proper loading of ML files;
changeset
wenzelm [Thu, 31 May 2007 14:34:06 +0200] rev 23155
proper loading of ML files;
Thu, 31 May 2007 14:34:05 +0200 tuned header;
changeset
wenzelm [Thu, 31 May 2007 14:34:05 +0200] rev 23154
tuned header;
Thu, 31 May 2007 14:24:27 +0200 tuned oracle setup;
changeset
wenzelm [Thu, 31 May 2007 14:24:27 +0200] rev 23153
tuned oracle setup;
Thu, 31 May 2007 14:01:58 +0200 moved HOLCF tools to canonical place;
changeset
wenzelm [Thu, 31 May 2007 14:01:58 +0200] rev 23152
moved HOLCF tools to canonical place;
Thu, 31 May 2007 13:24:13 +0200 moved TFL files to canonical place;
changeset
wenzelm [Thu, 31 May 2007 13:24:13 +0200] rev 23151
moved TFL files to canonical place;
Thu, 31 May 2007 13:18:52 +0200 moved TFL files to canonical place;
changeset
wenzelm [Thu, 31 May 2007 13:18:52 +0200] rev 23150
moved TFL files to canonical place;
Thu, 31 May 2007 13:18:42 +0200 added src/Tools;
changeset
wenzelm [Thu, 31 May 2007 13:18:42 +0200] rev 23149
added src/Tools; moved TFL files to canonical place;
Thu, 31 May 2007 13:00:56 +0200 fixed title;
changeset
wenzelm [Thu, 31 May 2007 13:00:56 +0200] rev 23148
fixed title;
Thu, 31 May 2007 12:59:31 +0200 Tools: generic tools outside of Pure.
changeset
wenzelm [Thu, 31 May 2007 12:59:31 +0200] rev 23147
Tools: generic tools outside of Pure.
Thu, 31 May 2007 12:06:31 +0200 moved Integ files to canonical place;
changeset
wenzelm [Thu, 31 May 2007 12:06:31 +0200] rev 23146
moved Integ files to canonical place;
Thu, 31 May 2007 11:00:06 +0200 fixed use_thy "LocalWeakening";
changeset
wenzelm [Thu, 31 May 2007 11:00:06 +0200] rev 23145
fixed use_thy "LocalWeakening";
Thu, 31 May 2007 10:17:23 +0200 included new example in the compiling process
changeset
urbanc [Thu, 31 May 2007 10:17:23 +0200] rev 23144
included new example in the compiling process
Thu, 31 May 2007 09:48:20 +0200 a theory using locally nameless terms and strong induction principles
changeset
urbanc [Thu, 31 May 2007 09:48:20 +0200] rev 23143
a theory using locally nameless terms and strong induction principles
Thu, 31 May 2007 09:14:14 +0200 tuned the proof
changeset
urbanc [Thu, 31 May 2007 09:14:14 +0200] rev 23142
tuned the proof
Thu, 31 May 2007 01:36:08 +0200 emulate later version of TextIO.inputLine;
changeset
wenzelm [Thu, 31 May 2007 01:36:08 +0200] rev 23141
emulate later version of TextIO.inputLine;
Thu, 31 May 2007 01:25:35 +0200 reversed SML B library patches;
changeset
wenzelm [Thu, 31 May 2007 01:25:35 +0200] rev 23140
reversed SML B library patches;
Thu, 31 May 2007 01:25:24 +0200 TextIO.inputLine: use present SML B library version;
changeset
wenzelm [Thu, 31 May 2007 01:25:24 +0200] rev 23139
TextIO.inputLine: use present SML B library version;
Wed, 30 May 2007 23:32:54 +0200 tuned USEDIR_OPTIONS;
changeset
wenzelm [Wed, 30 May 2007 23:32:54 +0200] rev 23138
tuned USEDIR_OPTIONS; PDF_VIEWER: try to be smart for MacOS (Darwin);
Wed, 30 May 2007 23:31:57 +0200 removed HOL4 image, which seldom works;
changeset
wenzelm [Wed, 30 May 2007 23:31:57 +0200] rev 23137
removed HOL4 image, which seldom works;
Wed, 30 May 2007 21:09:18 +0200 simplified data setup
changeset
haftmann [Wed, 30 May 2007 21:09:18 +0200] rev 23136
simplified data setup
Wed, 30 May 2007 21:09:17 +0200 instance: always print sorts on failure
changeset
haftmann [Wed, 30 May 2007 21:09:17 +0200] rev 23135
instance: always print sorts on failure
Wed, 30 May 2007 21:09:16 +0200 more example
changeset
haftmann [Wed, 30 May 2007 21:09:16 +0200] rev 23134
more example
Wed, 30 May 2007 21:09:15 +0200 fixed typo
changeset
haftmann [Wed, 30 May 2007 21:09:15 +0200] rev 23133
fixed typo
Wed, 30 May 2007 21:09:13 +0200 updated
changeset
haftmann [Wed, 30 May 2007 21:09:13 +0200] rev 23132
updated
Wed, 30 May 2007 21:09:12 +0200 generalized lemmas
changeset
haftmann [Wed, 30 May 2007 21:09:12 +0200] rev 23131
generalized lemmas
Wed, 30 May 2007 21:09:11 +0200 eliminated strings
changeset
haftmann [Wed, 30 May 2007 21:09:11 +0200] rev 23130
eliminated strings
Wed, 30 May 2007 21:09:09 +0200 tuned
changeset
haftmann [Wed, 30 May 2007 21:09:09 +0200] rev 23129
tuned
Wed, 30 May 2007 18:05:10 +0200 clarified error message
changeset
krauss [Wed, 30 May 2007 18:05:10 +0200] rev 23128
clarified error message
Wed, 30 May 2007 02:41:26 +0200 simplify names of locale interpretations
changeset
huffman [Wed, 30 May 2007 02:41:26 +0200] rev 23127
simplify names of locale interpretations
Wed, 30 May 2007 01:53:38 +0200 renamed some lemmas in Complex.thy
changeset
huffman [Wed, 30 May 2007 01:53:38 +0200] rev 23126
renamed some lemmas in Complex.thy
Wed, 30 May 2007 01:46:05 +0200 cleaned up proofs; reorganized sections; removed redundant lemmas
changeset
huffman [Wed, 30 May 2007 01:46:05 +0200] rev 23125
cleaned up proofs; reorganized sections; removed redundant lemmas
Tue, 29 May 2007 20:53:13 +0200 use new-style instance declarations
changeset
huffman [Tue, 29 May 2007 20:53:13 +0200] rev 23124
use new-style instance declarations
Tue, 29 May 2007 20:31:53 +0200 instance complex :: banach
changeset
huffman [Tue, 29 May 2007 20:31:53 +0200] rev 23123
instance complex :: banach
Tue, 29 May 2007 20:31:42 +0200 add lemma real_sqrt_sum_squares_less
changeset
huffman [Tue, 29 May 2007 20:31:42 +0200] rev 23122
add lemma real_sqrt_sum_squares_less
Tue, 29 May 2007 18:31:30 +0200 cleaned up some proofs
changeset
huffman [Tue, 29 May 2007 18:31:30 +0200] rev 23121
cleaned up some proofs
Tue, 29 May 2007 18:19:56 +0200 interpretation bounded_linear_divide
changeset
huffman [Tue, 29 May 2007 18:19:56 +0200] rev 23120
interpretation bounded_linear_divide
Tue, 29 May 2007 17:37:04 +0200 add bounded_linear lemmas
changeset
huffman [Tue, 29 May 2007 17:37:04 +0200] rev 23119
add bounded_linear lemmas
Tue, 29 May 2007 17:36:35 +0200 add isUCont lemmas
changeset
huffman [Tue, 29 May 2007 17:36:35 +0200] rev 23118
add isUCont lemmas
Tue, 29 May 2007 14:03:49 +0200 updated examples to include an instance of (lexicographic_order simp:...)
changeset
krauss [Tue, 29 May 2007 14:03:49 +0200] rev 23117
updated examples to include an instance of (lexicographic_order simp:...)
Mon, 28 May 2007 16:30:28 +0200 Complex: generalized type of exp
changeset
huffman [Mon, 28 May 2007 16:30:28 +0200] rev 23116
Complex: generalized type of exp
Mon, 28 May 2007 16:29:17 +0200 generalized exp to work over any complete field; new proof of exp_add
changeset
huffman [Mon, 28 May 2007 16:29:17 +0200] rev 23115
generalized exp to work over any complete field; new proof of exp_add
Mon, 28 May 2007 16:27:33 +0200 add type annotations for exp
changeset
huffman [Mon, 28 May 2007 16:27:33 +0200] rev 23114
add type annotations for exp
Mon, 28 May 2007 04:22:44 +0200 interpretations additive_scaleR_left, additive_scaleR_right
changeset
huffman [Mon, 28 May 2007 04:22:44 +0200] rev 23113
interpretations additive_scaleR_left, additive_scaleR_right
Mon, 28 May 2007 03:45:41 +0200 remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
changeset
huffman [Mon, 28 May 2007 03:45:41 +0200] rev 23112
remove division_by_zero requirement from termdiffs lemmas; cleaned up some proofs
Sun, 27 May 2007 20:04:02 +0200 new proof of Cauchy product formula for series
changeset
huffman [Sun, 27 May 2007 20:04:02 +0200] rev 23111
new proof of Cauchy product formula for series
Sat, 26 May 2007 07:26:03 +0200 What it says
changeset
nipkow [Sat, 26 May 2007 07:26:03 +0200] rev 23110
What it says
Fri, 25 May 2007 21:08:53 +0200 improved error handling
changeset
haftmann [Fri, 25 May 2007 21:08:53 +0200] rev 23109
improved error handling
Fri, 25 May 2007 21:08:52 +0200 using rudimentary class target mechanism
changeset
haftmann [Fri, 25 May 2007 21:08:52 +0200] rev 23108
using rudimentary class target mechanism
Fri, 25 May 2007 21:08:46 +0200 *** empty log message ***
changeset
haftmann [Fri, 25 May 2007 21:08:46 +0200] rev 23107
*** empty log message ***
Fri, 25 May 2007 21:08:45 +0200 fixed typo
changeset
haftmann [Fri, 25 May 2007 21:08:45 +0200] rev 23106
fixed typo
Fri, 25 May 2007 18:25:17 +0200 fix typos
changeset
huffman [Fri, 25 May 2007 18:25:17 +0200] rev 23105
fix typos
Fri, 25 May 2007 18:24:11 +0200 *** empty log message ***
changeset
nipkow [Fri, 25 May 2007 18:24:11 +0200] rev 23104
*** empty log message ***
Fri, 25 May 2007 18:11:25 +0200 *** empty log message ***
changeset
nipkow [Fri, 25 May 2007 18:11:25 +0200] rev 23103
*** empty log message ***
Fri, 25 May 2007 18:10:56 +0200 *** empty log message ***
changeset
nipkow [Fri, 25 May 2007 18:10:56 +0200] rev 23102
*** empty log message ***
Fri, 25 May 2007 18:08:47 +0200 tuned
changeset
nipkow [Fri, 25 May 2007 18:08:47 +0200] rev 23101
tuned
Fri, 25 May 2007 18:08:34 +0200 Added List_Comprehension
changeset
nipkow [Fri, 25 May 2007 18:08:34 +0200] rev 23100
Added List_Comprehension
Fri, 25 May 2007 06:06:49 +0200 adapted to fix for fresh_fun_simp
changeset
urbanc [Fri, 25 May 2007 06:06:49 +0200] rev 23099
adapted to fix for fresh_fun_simp
Fri, 25 May 2007 05:18:56 +0200 took out Class.thy from the compiling process until memory problems are solved
changeset
urbanc [Fri, 25 May 2007 05:18:56 +0200] rev 23098
took out Class.thy from the compiling process until memory problems are solved
Fri, 25 May 2007 00:36:54 +0200 simplify some proofs
changeset
huffman [Fri, 25 May 2007 00:36:54 +0200] rev 23097
simplify some proofs
Thu, 24 May 2007 22:55:53 +0200 *** empty log message ***
changeset
nipkow [Thu, 24 May 2007 22:55:53 +0200] rev 23096
*** empty log message ***
Thu, 24 May 2007 16:52:54 +0200 Squared things out.
changeset
obua [Thu, 24 May 2007 16:52:54 +0200] rev 23095
Squared things out.
Thu, 24 May 2007 14:04:06 +0200 fix a bug : the semantics of no_asm was the opposite
changeset
narboux [Thu, 24 May 2007 14:04:06 +0200] rev 23094
fix a bug : the semantics of no_asm was the opposite
Thu, 24 May 2007 13:59:54 +0200 temporary fix for a bug in fresh_fun_simp
changeset
urbanc [Thu, 24 May 2007 13:59:54 +0200] rev 23093
temporary fix for a bug in fresh_fun_simp
Thu, 24 May 2007 12:09:38 +0200 formalisation of my PhD (the result was correct, but the proof needed several corrections)
changeset
urbanc [Thu, 24 May 2007 12:09:38 +0200] rev 23092
formalisation of my PhD (the result was correct, but the proof needed several corrections)
Thu, 24 May 2007 12:00:47 +0200 add an option in fresh_fun_simp to prevent rewriting in assumptions
changeset
narboux [Thu, 24 May 2007 12:00:47 +0200] rev 23091
add an option in fresh_fun_simp to prevent rewriting in assumptions
Thu, 24 May 2007 08:37:43 +0200 fixes tvar issue in type inference
changeset
haftmann [Thu, 24 May 2007 08:37:43 +0200] rev 23090
fixes tvar issue in type inference
Thu, 24 May 2007 08:37:42 +0200 tuned
changeset
haftmann [Thu, 24 May 2007 08:37:42 +0200] rev 23089
tuned
(0) -10000 -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle