src/HOL/Eisbach/Eisbach.thy
changeset 61918 0f9e0106c378
parent 61853 fb7756087101
child 62134 2405ab06d5b1
equal deleted inserted replaced
61917:35ec3757d3c1 61918:0f9e0106c378
    17 
    17 
    18 ML_file "parse_tools.ML"
    18 ML_file "parse_tools.ML"
    19 ML_file "method_closure.ML"
    19 ML_file "method_closure.ML"
    20 ML_file "eisbach_rule_insts.ML"
    20 ML_file "eisbach_rule_insts.ML"
    21 ML_file "match_method.ML"
    21 ML_file "match_method.ML"
    22 ML_file "eisbach_antiquotations.ML"
       
    23 
    22 
    24 method solves methods m = (m; fail)
    23 method solves methods m = (m; fail)
    25 
    24 
    26 end
    25 end