2014-12-05 haftmann [Fri, 05 Dec 2014 19:35:36 +0100] rev 59104
allow multiple inheritance of targets
src/Doc/Codegen/Adaptation.thy src/HOL/Imperative_HOL/Heap_Monad.thy src/HOL/Quickcheck_Narrowing.thy src/HOL/Quickcheck_Random.thy src/Tools/Code/code_haskell.ML src/Tools/Code/code_ml.ML src/Tools/Code/code_runtime.ML src/Tools/Code/code_scala.ML src/Tools/Code/code_target.ML

2014-12-04 haftmann [Thu, 04 Dec 2014 16:51:54 +0100] rev 59103
tuned module structure
src/Tools/Code/code_namespace.ML src/Tools/Code/code_printer.ML src/Tools/Code/code_target.ML

2014-12-04 haftmann [Thu, 04 Dec 2014 16:51:54 +0100] rev 59102
tuned data structures
src/Tools/Code/code_target.ML

2014-12-04 haftmann [Thu, 04 Dec 2014 16:51:54 +0100] rev 59101
tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge;
n. b. merging of bidirectional dependencies results in effective join of involved nodes: no termination problem since ancestry is always kept explicitly normalized
src/Tools/Code/code_target.ML

2014-12-04 haftmann [Thu, 04 Dec 2014 16:51:54 +0100] rev 59100
tuned
src/Tools/Code/code_target.ML

2014-12-04 haftmann [Thu, 04 Dec 2014 16:51:54 +0100] rev 59099
tuned names
src/Tools/Code/code_target.ML

2014-12-04 haftmann [Thu, 04 Dec 2014 16:51:54 +0100] rev 59098
eta-expand all search patterns using schematic place holders
src/Pure/Tools/find_theorems.ML

2014-12-04 haftmann [Thu, 04 Dec 2014 16:51:54 +0100] rev 59097
revert "better" handling of abbreviation from c61fe520602b
src/Pure/Tools/find_theorems.ML

2014-12-04 haftmann [Thu, 04 Dec 2014 16:51:54 +0100] rev 59096
tuned variable names
src/Pure/Tools/find_theorems.ML

2014-12-04 haftmann [Thu, 04 Dec 2014 16:51:54 +0100] rev 59095
turn application-specific Pattern.matches_subterm into an application-private function
src/Pure/Tools/find_theorems.ML src/Pure/more_pattern.ML