author | haftmann |
Tue, 20 Jun 2017 08:01:56 +0200 | |
changeset 66125 | 28e782dd0278 |
parent 66124 | 7f0088571576 |
child 66126 | 60bf6934fabd |
--- a/src/Pure/Isar/code.ML Tue Jun 20 08:01:56 2017 +0200 +++ b/src/Pure/Isar/code.ML Tue Jun 20 08:01:56 2017 +0200 @@ -165,6 +165,7 @@ fun case_consts_of (Constructors (_, case_consts)) = case_consts | case_consts_of (Abstractor _) = []; + (* functions *) datatype fun_spec = Eqns_Default of (thm * bool) list * (thm * bool) list lazy