src/HOL/HOL.ML
changeset 9396 a1b31d61f8e1
parent 7529 fa534e4f7e49
child 9970 dfe4747c8318
equal deleted inserted replaced
9395:1c9851cdfe9f 9396:a1b31d61f8e1
     1 
       
     2 structure HOL =
     1 structure HOL =
     3 struct
     2 struct
     4   val thy = the_context ();
     3   val thy = the_context ();
     5   val plusI = plusI;
     4   val plusI = plusI;
     6   val minusI = minusI;
     5   val minusI = minusI;