Fri, 10 Mar 2017 23:16:40 +0100 | immler | modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas | changeset | files |
Sun, 12 Mar 2017 19:06:10 +0100 | wenzelm | proper edits; | changeset | files |
Sun, 12 Mar 2017 18:50:02 +0100 | wenzelm | suppress vacuous messages; | changeset | files |
Sun, 12 Mar 2017 18:45:53 +0100 | wenzelm | clarified modules; | changeset | files |
Sun, 12 Mar 2017 18:05:06 +0100 | wenzelm | more explicit message type: allows body to become empty; | changeset | files |
Sun, 12 Mar 2017 17:59:03 +0100 | wenzelm | clarified current_command: index refers to node content, negative index means first command; | changeset | files |
Sun, 12 Mar 2017 14:43:50 +0100 | wenzelm | clarified caret offset; | changeset | files |