equal
deleted
inserted
replaced
135 val setup = |
135 val setup = |
136 Context.theory_map (Function_Common.set_preproc sequential_preproc) |
136 Context.theory_map (Function_Common.set_preproc sequential_preproc) |
137 |
137 |
138 |
138 |
139 val fun_config = FunctionConfig { sequential=true, default=NONE, |
139 val fun_config = FunctionConfig { sequential=true, default=NONE, |
140 domintros=false, partials=false, tailrec=false } |
140 domintros=false, partials=false } |
141 |
141 |
142 fun gen_add_fun add fixes statements config lthy = |
142 fun gen_add_fun add fixes statements config lthy = |
143 let |
143 let |
144 fun pat_completeness_auto ctxt = |
144 fun pat_completeness_auto ctxt = |
145 Pat_Completeness.pat_completeness_tac ctxt 1 |
145 Pat_Completeness.pat_completeness_tac ctxt 1 |