Mercurial
isabelle
/ changelog
summary
|
shortlog
| changelog |
graph
|
tags
|
branches
|
files
|
gz
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
+10
+30
+100
+300
+1000
tip
8 months ago
blanchet [Sat, 08 Sep 2012 22:54:37 +0200] rev 49226
fixed and enabled iterator/recursor theorems
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
src/HOL/Codatatype/Tools/bnf_fp_util.ML
8 months ago
blanchet [Sat, 08 Sep 2012 21:52:17 +0200] rev 49225
renamed for consistency
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
8 months ago
blanchet [Sat, 08 Sep 2012 21:37:23 +0200] rev 49224
oops
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
8 months ago
blanchet [Sat, 08 Sep 2012 21:33:15 +0200] rev 49223
tuning
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_wrap.ML
8 months ago
blanchet [Sat, 08 Sep 2012 21:30:31 +0200] rev 49222
for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants
src/HOL/Codatatype/Examples/HFset.thy
src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy
src/HOL/Codatatype/Examples/Lambda_Term.thy
src/HOL/Codatatype/Examples/ListF.thy
src/HOL/Codatatype/Examples/Process.thy
src/HOL/Codatatype/Examples/Stream.thy
src/HOL/Codatatype/Examples/TreeFI.thy
src/HOL/Codatatype/Examples/TreeFsetI.thy
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
8 months ago
blanchet [Sat, 08 Sep 2012 21:21:27 +0200] rev 49221
fixed bug with one-value types with phantom type arguments
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
8 months ago
blanchet [Sat, 08 Sep 2012 21:04:27 +0200] rev 49220
imported patch debugging
src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy
src/HOL/Codatatype/Examples/Lambda_Term.thy
src/HOL/Codatatype/Examples/ListF.thy
src/HOL/Codatatype/Examples/Process.thy
src/HOL/Codatatype/Examples/Stream.thy
src/HOL/Codatatype/Examples/TreeFI.thy
src/HOL/Codatatype/Examples/TreeFsetI.thy
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
8 months ago
blanchet [Sat, 08 Sep 2012 21:04:26 +0200] rev 49219
repaired "nofail4" example
src/HOL/Codatatype/Examples/Misc_Data.thy
8 months ago
blanchet [Sat, 08 Sep 2012 21:04:26 +0200] rev 49218
renamed xxxBNF to pre_xxx
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
src/HOL/Codatatype/Tools/bnf_fp_util.ML
8 months ago
blanchet [Sat, 08 Sep 2012 21:04:26 +0200] rev 49217
fixed handling of map of "fun"
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
(0)
-30000
-10000
-3000
-1000
-300
-100
-30
-10
+10
+30
+100
+300
+1000
tip