| 2009-11-10 |
huffman |
add lemma parallel_fix_ind
|
file |
diff |
annotate
|
| 2009-05-08 |
huffman |
rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
|
file |
diff |
annotate
|
| 2008-12-17 |
huffman |
remove cvs Id tags
|
file |
diff |
annotate
|
| 2008-06-22 |
huffman |
use new-style abbreviation/notation for fix syntax
|
file |
diff |
annotate
|
| 2008-06-18 |
huffman |
add lemma iterate_iterate
|
file |
diff |
annotate
|
| 2008-06-12 |
huffman |
change orientation of fix_eqI and convert to rule_format;
|
file |
diff |
annotate
|
| 2008-01-18 |
huffman |
add space to binder syntax
|
file |
diff |
annotate
|
| 2008-01-18 |
huffman |
change lemma admD to rule_format
|
file |
diff |
annotate
|
| 2007-10-21 |
wenzelm |
modernized specifications ('definition', 'abbreviation', 'notation');
|
file |
diff |
annotate
|
| 2005-11-05 |
huffman |
add proof of Bekic's theorem: fix_cprod
|
file |
diff |
annotate
|
| 2005-11-05 |
huffman |
put iterate and fix in separate sections; added Letrec
|
file |
diff |
annotate
|
| 2005-11-05 |
huffman |
renamed and added ch2ch, cont2cont, mono2mono theorems ending in _fun, _lambda, _LAM
|
file |
diff |
annotate
|
| 2005-11-04 |
huffman |
moved adm_chfindom from Fix.thy to Cfun.thy; moved admw-related stuff to its own section
|
file |
diff |
annotate
|
| 2005-11-03 |
huffman |
change syntax for LAM to use expressions as patterns; define LAM pattern syntax for cpair, spair, sinl, sinr, up
|
file |
diff |
annotate
|
| 2005-11-02 |
huffman |
reorganized; removed intermediate constant Ifix; changed iterate to a continuous type; added theorem fix_least_less
|
file |
diff |
annotate
|
| 2005-10-10 |
huffman |
new syntax translations for continuous lambda abstraction
|
file |
diff |
annotate
|
| 2005-09-22 |
huffman |
cleaned up
|
file |
diff |
annotate
|
| 2005-07-26 |
huffman |
add theorem fix_defined_iff; cleaned up
|
file |
diff |
annotate
|
| 2005-06-23 |
huffman |
added theorems fix_strict, fix_defined, fix_id, fix_const
|
file |
diff |
annotate
|
| 2005-06-14 |
huffman |
renamed theorem cont2cont_CF1L_rev2 to cont2cont_lambda
|
file |
diff |
annotate
|
| 2005-06-03 |
huffman |
cleaned up proof of cont_Ifix
|
file |
diff |
annotate
|
| 2005-05-26 |
huffman |
added defaultsort declaration
|
file |
diff |
annotate
|
| 2005-05-25 |
huffman |
moved adm_chfindom from Adm.thy to Fix.thy, to remove dependence on Cfun
|
file |
diff |
annotate
|
| 2005-05-25 |
wenzelm |
removed LICENCE note -- everything is subject to Isabelle licence as
|
file |
diff |
annotate
|
| 2005-05-24 |
huffman |
Moved admissibility definitions and lemmas to a separate theory
|
file |
diff |
annotate
|
| 2005-05-18 |
huffman |
shortened proof of adm_disj
|
file |
diff |
annotate
|
| 2005-05-18 |
huffman |
cleaned up and shortened some proofs
|
file |
diff |
annotate
|
| 2005-04-26 |
huffman |
Added binder syntax for fix
|
file |
diff |
annotate
|
| 2005-03-30 |
huffman |
changed comments to text blocks, cleaned up a few proofs
|
file |
diff |
annotate
|
| 2005-03-04 |
huffman |
fix headers
|
file |
diff |
annotate
|