Mercurial
isabelle
/ changelog
summary
|
shortlog
| changelog |
graph
|
tags
|
branches
|
files
|
gz
2012-09-14
wenzelm [Fri, 14 Sep 2012 21:23:06 +0200] rev 49373
merged
2012-09-14
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49372
polished the induction
src/HOL/Codatatype/BNF_FP.thy
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
2012-09-14
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49371
put the flat at the right place (to avoid exceptions)
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
2012-09-14
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49370
fixed variable exporting problem
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
2012-09-14
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49369
compile
src/HOL/Codatatype/Examples/Stream.thy
src/HOL/Codatatype/Examples/TreeFsetI.thy
2012-09-14
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49368
added induct tactic
src/HOL/Codatatype/BNF_FP.thy
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
2012-09-14
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49367
tuning
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
2012-09-14
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49366
renamed "mk_UnN" to "mk_UnIN"
src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
src/HOL/Codatatype/Tools/bnf_util.ML
2012-09-14
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49365
merged two commands
NEWS
src/Doc/Sledgehammer/document/root.tex
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
2012-09-14
blanchet [Fri, 14 Sep 2012 12:09:27 +0200] rev 49364
allow default values to refer to selector arguments -- this is useful, e.g. for tllist: ttl (TNil x) = TNil x (example by Andreas Lochbihler)
src/HOL/Codatatype/Tools/bnf_wrap.ML