Diffusion Isabelle 17090e27aae9

more scalable data structure (but: rarely used with > 5 arguments);
17090e27aae9
Actions

Tags

None

Subscribers

None

Description

more scalable data structure (but: rarely used with > 5 arguments);

Details

Provenance

Authored on

Parents

rISABELLEf54b061c2c22: merged

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLE17090e27aae9: more scalable data structure (but: rarely used with > 5 arguments);.Aug 26 2021, 2:45 PM

Changes (18)

Path

Size

src/

Doc/

Implementation/

HOL/

Eisbach/

match_method.ML

Library/

Tools/

BNF/

bnf_fp_def_sugar.ML

bnf_gfp_rec_sugar_tactics.ML

Ctr_Sugar/

ctr_sugar_code.ML

Function/

induction_schema.ML

SMT/

smt_replay_methods.ML

Transfer/

Pure/

Isar/

rISABELLE17090e27aae9

src/Doc/Implementation/Logic.thy

Loading...

src/HOL/Eisbach/match_method.ML

Loading...

src/HOL/Library/cconv.ML

Loading...

src/HOL/Library/code_lazy.ML

Loading...

src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

Loading...

src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML

Loading...

src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML

Loading...

src/HOL/Tools/Function/induction_schema.ML

Loading...

src/HOL/Tools/SMT/smt_replay_methods.ML

Loading...

src/HOL/Tools/Transfer/transfer.ML

Loading...

src/Pure/Isar/local_defs.ML

Loading...

src/Pure/drule.ML

Loading...

src/Pure/goal.ML

Loading...

src/Pure/more_thm.ML

Loading...

src/Pure/proofterm.ML

Loading...

src/Pure/term_subst.ML

Loading...

src/Pure/thm.ML

Loading...

src/Pure/variable.ML

Loading...