src/Tools/isac/Knowledge/Simplify.thy
changeset 60291 52921aa0e14a
parent 60290 bb4e8b01b072
child 60303 815b0dc8b589
     1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Thu Jun 10 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Thu Jun 10 12:48:50 2021 +0200
     1.3 @@ -20,9 +20,6 @@
     1.4    Simplify    :: "real => real"  (*"Simplify (1+2a+3+4a)*)
     1.5    Vereinfache :: "real => real"  (*"Vereinfache (1+2a+3+4a)*)
     1.6  
     1.7 -ML \<open>
     1.8 -val thy = @{theory};
     1.9 -\<close>
    1.10  (** problems **)
    1.11  setup \<open>KEStore_Elems.add_pbts
    1.12    [(Problem.prep_input @{theory} "pbl_simp" [] Problem.id_empty